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.
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?