This is a fantastic metaphor for what's otherwise a superpower. Imagine being able to have the computer do the hard work of being able to find design bugs for you!This is better than any abstract diagram or design document meant solely for human consumption. A computer can't automatically verify a Vizio diagram, check a design document for logical inconsistencies, or call out places where future work might conflict with current constraints.

"Formal specifications are beacons that illuminate the terrain"

"Good plans not only light the path forward, but show you where not to tread."This is very much akin to TDD as it doesn't just tell you what code to write but also when to stop. It's a system design tool using code!

What Does A Good Plan Do?

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

What's A Good Plan And Why?

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

What Are Formal Specifications And What Do They Look Like

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

Why Do Planning At All? Isn't That Waterfall?

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

What Does Success Look Like?

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

Why Don't More People Use Formal Methods Like Specification?

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

How Can You Get Started With This Software Superpower?

These ideas have greatly influenced my software practice and helped me to build better systems than before. 

Learn how formal specifications can help light the way forward on complex software projects by identifying software bugs ahead of implementation.

Using formal methods to plan software with flare

Jonathan Magen