Why Alloy?

I want to share with you the most amazing description of software development I’ve ever read:¹

The process of software development should be straightforward. First, you design the abstractions, from a careful consideration of the problem to be solved and its likely future variants. Then you develop its embodiments in code: the interfaces and modules, data structures and algorithms (or in object-oriented parlance, the class hierarchy, datatype representations, and methods).

Unfortunately, this approach rarely works. […] You come up with a collection of abstractions that seem to be simple and robust. But when you implement them, they turn out to be incoherent and perhaps even inconsistent, and they crumble in complexity as you attempt to adapt them as the code grows.

Why are the flaws that escaped you at design time so blindingly obvious (and painful) at coding time? It is surely not because the abstractions you chose were perfect in every respect except for their realizability in code. Rather, it was because the environment of programming is so much more exacting than the environment of sketching design abstractions. […]

But code is a poor medium for exploring abstractions. The demands of executability add a web of complexity, so that even a simple abstraction becomes mired in a bog of irrelevant details. […] An alternative approach is to attack the design of abstractions head-on, with a notation chosen for ease of expression and exploration. By making the notation precise and unambiguous, the risk of wishful thinking is reduced.

This approach [is] known as formal specification.

This is the introduction to the book Software Abstractions by Daniel Jackson, and the moment I read it, I was sold. Never had I heard a description of software development that so completely fit my experiences and frustrations in the field.

And better? The rest the book was an exploration of and meditation on Alloy; Jackson’s own language and analyzer that promised to address these shortcomings of modeling abstraction.

Prescient enumeration of some difficulty bundled with a promised solution? Heck yeah! Let’s go!

Stumbling Around

Unfortunately, the introduction was the only part of the book I was able to understand. Specification is a concept intrinsically tied to logic — and not the boolean logic I was familiar with as a programmer.

No, this was a heady mix of propositional, prepositional, and relational logic. Logic that trafficked in set theory and novel notation like ∀, ∃, ∈, and ⊃. It was wholly unfamiliar territory that nonetheless employed just enough common terminology to be more confusing than the mere unknown.

Further, once I had enough knowledge of the language to string some words together, I quickly realized I couldn’t see the abstractions I wished to model in clear enough light to properly describe them. And even were I able to, I didn’t understand the whens, wheres, and whys of specifications well enough to know when it would be most advantageous or efficient to do so.

So I set the book aside for some later date when I’d be able to give it the attention needed to unlock its secrets.

The Time is Now

Which brings us to the present. This year’s project is to:

1. Do the work to make Software Abstractions make sense to an uneducated dev like me. And then,
2. Wrap any learnings up into a handy primer for the next person who would like to get to there from here.

I’ll be posting about what I learn weekly, but I suspect the project will unfold in three general arcs:

Understanding Logic(s)

There are a number of formal logics at play in the Alloy language. Identifying them, understanding them, and grokking their utility vs. computational expressions will be the first order of business.

Unlocking Alloy Analyzer

The Alloy Analyzer program, which (as I understand it) turns constraints expressed in the Alloy language into models that can be checked for satisfiability, has many quirks of its own. Some amount of mucking about will be necessary just to figure out how to produce output. Then even more mucking to determine how to interpret it.

What Models, When?

Once fluent in expressing models to Alloy and interpreting the results, I’ll need answer the big question: “How do I use this to make my programs better?”

If we take Mr. Jackson at his word, code is a poor medium for exploring abstractions and Alloy a rich one. How does my planning/development/code get better when I stop futzing about with a bad tool and use the right one instead?

Setting Expectations

As you can probably tell from many of the hand-wavy explanations above, I don’t know what I’m talking about, here. That’s okay. Learning what I’m talking about is the job.

But my estimates of what I can get done in a year may be wildly off. It could be I never get past “Understanding Logic”, above.

That’s okay, too. One of my favorite books is Jeremy Kun’s A Programmer’s Introduction to Mathematics. If the only thing to come out of 2023 is my hacky version of A Programmer’s Introduction to Predicate Logic, I’ll consider this a success.

Hope you will, too.