Using formal methods to plan software with flare

The article is very concise when it comes to describing good plans.

"In software engineering, these flares take the form of formal specifications, or blueprints that describe, analyze, and verify a system design. Often, we spend the bulk of our coding time tinkering with plumbing and fiddly bits; the essential behavior we’re trying to program is just a small part of the equation. Making sure the essential behavior is correct before you start a project can save a lot of time and energy down the road."

"Typically, specifications are written in formal specification languages such as TLA+ or Alloy. While programming languages are designed to be run, specification languages are designed to be simulated, and therefore include features like nondeterminism (this call can succeed or fail), atomicity (the server can crash between these two calls), and scalability (10 servers will be trying to make this call). Specification languages can also delineate the parts of the spec you’ve carefully thought through, as well as the parts you’ve shunted to the side for the time being.

Weeks of coding can save you hours of planning. Agile doesn't mean you don't plan, it just means you don't overplan and avoid sticking to plans that don't work.

"It might be annoying to throw out a mostly working plan, but it’s far worse to throw out a mostly working codebase."

Planning with formal specification techniques can be done iteratively to avoid costly big-bang and waterfall design practices such as Big Design Up Front (BDUF).

"The formal specifications had done their job, illuminating several possible paths down the hill. Now it was time to apply a little good old-fashioned reasoning. After some discussion with the project manager about our timeline and scope, we settled on a single design and got to work."

Good tools center human judgement by making it more effective. Bad tools make assumptions about completeness that end up remove human judgement entirely. This is a perpetual conflict in the Pure Automation vs. Augmentation discussion.

The author writes:

"I came away from the experience wondering why formal specification wasn’t more widespread. It had proved valuable at our startup, which had just 10 engineers. How much might it help development teams building software at scale? Through research, I discovered UX issues are the primary barrier: The tools are hard to learn, hard to use, and their benefits might not be immediately obvious to users. These are genuine problems, but addressable ones."

There are tons of resources available for TLA+ and Alloy, the two most popular tools for formal specification.

If you want a deep dive into TLA+ you can get started by buying the author's book, Practical TLA+. It's an excellent read

There is also currently a book underway by Daniel Jackson and his team to introduce the exciting new features of Alloy 6. Released in Fall of 2021, Alloy 6 introduces a variety of new capabilities which make it especially attractive for this sort of work.