aerkiaga's blog

So much has happened since my last blog post. My Google Summer of Code project was successful. I got a medical degree and ranked among the top 1% in public healthcare medical examinations. Did some research on ultrasound imaging and made a few prototypes (one manufacturer has offered to support my next prototype).

I've become more proficient in Rust and learnt Verilog and Chisel, which I use to program FPGAs for my ultrasound devices.

As for my programming projects, these years I've slowly expanded nodeverse, my voxel-based videogame. But my largest projects by far have been formal verification-related; I learnt Coq, and latter attempted to create my own language for formal verification: Rooster. After working on it for some time, I had collected a lot of knowledge on the design of these kinds of languages, and programming languages in general. Last year, after a lengthy design phase, I finally felt comfortable enough to go on to create Nacre.

I will probably talk more about this Nacre language in future posts, but for now I would just like to make an overview of its completion status and goals. Right now the compiler is almost fully functional, with a complete type checking kernel, the parser only missing some features, and code generation disabled by default for now but steadily progressing. Right now I'm implementing a specialization pass at the IR level.

The end goal is to get a language that one can use to write specific critical parts of a larger project in a formally verified fashion, letting the build system handle compiler invocation and linking.