One Year of Writing Fault

This was a side project I thought I would get stuck on or bored of in a few months. One year later it feels like it might be the tool for systems I’ve always wanted.

Calendar vector created by freepik

Now that we’re starting to socialize in person again, people who I have relationships with based solely on traveling in the same circles and running into them at the same happy hours are starting to come back into my life. The first thing they always want to know is: “Are you still working on that programming language? How is that going?”

The Backstory

For those of you who haven’t been following my descent down the rabbit hole of programming language design, here’s the thirty second summary:

A few years ago I started getting interested in how formal verification could be used to model systems rather than code correctness. I found formal verification itself to be difficult to understand but I couldn’t shake my interest in it and ended up learning a lot about boolean logic, SAT solvers and the SMT solvers derived from them. At some point I realized that the format SAT/SMT solvers need to solve logic puzzles looks structurally very similar to the format compilers produce. An obsession was born: can you write a compiler that takes a system spec and turns it into a logic puzzle an SMT solver can solve?

(Well actually the question was whether specifically I could do it, since there are a few specification languages like Alloy, Dafny, and Boogie that do just that. Only they maintain much of the structure of first order logic whereas I wanted to write code that felt more like programming)

So…. How’s It Going?

I cleared a major hurdle last month when I implemented assert statements. I actually figured this would be one of the easier parts of the process since assert statements are just boolean logic, so they are already in the format that the compiler needs to convert them to.

And then I realized that if I wanted an assert to cover the entire state space then assert x > 5; wasn’t enough. It needed to be (assert (> x_0 5)) (assert (> x_1 5)) (assert (> x_2 5)) … for every single static assignment variable in the model. I needed to do a cartesian product, and that took a bit to figure out but I did figure it out.