The Subtle Power of Booleans

Programming with truth and statefulness.

I like formal specification because I don’t really understand it. That is kind of my personality, curiosity blended with absolute raw stubbornness.

In my quest to understand formal specification I’ve started to learn more about logic programming than I did before. I first encountered logic programming when Pierre de Lacaze came to a meetup I belonged to and gave a talk about Prolog. I was fascinated, but couldn’t find any resources to learn how to use Prolog and was endlessly frustrated when every tutorial I did find stopped at building a Sudoku solver. This did not seem relevant to anything I wanted to do and so I never looked closely at it.

Alloy and SAT solvers

But logic programming doesn’t begin and end with tools like Prolog. One formal specification tool I like using is Alloy, which is basically just a nicer interface on top of a SAT (for SATISFIABILITY) solver. SAT solvers are programs that look for solutions that satisfy all the facts much in the same way that Prolog does. There are many different ways of implementing SAT solvers, this post is only the tip of the iceberg in that regard!

You write models in Alloy using a markup language that defines the spec around relationships. Alloy has signatures, which you can think of as a…