Why Every Programmer Needs a Blueprint: Reflections on Specification

“Writing is nature’s way of letting you know how sloppy your thinking is.” – Guindon

---

When I first started programming in 1957, the craft was a solitary act of translating ideas directly into code. Decades later, after a career in computer‑science research and the creation of the TLA+ specification language, I have come to see a striking parallel between software development and building construction: architects never raise a wall without a plan, yet many programmers begin typing without a single line of description.

The Core Argument: Specification as a Blueprint

A specification is the software analogue of an architect’s blueprint. It does not promise automatic code generation—buildings are not erected from drawings alone—but it provides a shared, stable reference that guides every subsequent decision. Two observations support this claim:

1. Thinking before doing – Writing forces us to confront the gaps in our understanding. If we cannot articulate what a program should accomplish, we cannot be confident that we truly grasp the problem.
2. Elevating the abstraction level – Most programming methods (test‑driven development, agile sprints, etc.) focus on how to code. Without a higher‑level view of what the system must achieve, we risk embedding design flaws that no amount of refactoring can easily remove.

From Prose to Formalism: A Spectrum of Specs

Specification is often equated with formal languages, yet the reality is a continuum:

• Informal specs – A couple of precise sentences are sufficient for trivial utilities. For example, a function that reads a file and returns its length can be described in plain English with a few mathematical symbols.
• Formal specs – Complex, concurrent, or distributed systems (think of a bridge rather than a garden shed) demand rigor. Formal tools such as model checkers can verify properties that informal prose cannot guarantee.

The key is not the language but the purpose: to capture the essential behavior while discarding irrelevant details.

Practical Benefits Demonstrated

In a recent project I needed a variation of the classic connected‑components algorithm. The modification was small, but subtle bugs emerged when I tried to debug the Java implementation. By writing a TLA+ spec and feeding it to the TLC model checker, I isolated the error in a day—far faster than chasing stack traces. The experience reinforced two points:

1. Design errors surface early when the system is described at a higher level.
2. Writing a formal spec improves informal documentation, because the discipline of precise description carries over to everyday comments.

Addressing Common Objections

“Specs are too costly for fast delivery.”

The time spent drafting a spec is an investment that pays off when the code is later modified. Without a spec, each change becomes a patch, and the cumulative complexity can force a complete rewrite.

“Requirements are vague; we can’t specify them.”

Vagueness itself demands clarification. By attempting to write a spec, we expose ambiguities and force stakeholders to refine their expectations. Even a set of six alignment rules for a pretty‑printer, as I once wrote, proved more manageable than 850 lines of ad‑hoc code.

“Tests are enough; they double as specifications.”

Tests verify instances of behavior, not the general contract. A test suite cannot guarantee that a concurrent algorithm is free of race conditions; only a proof or exhaustive model checking can provide that assurance.

Implications for Education and Practice

Specification should be a core component of computer‑science curricula, not an afterthought limited to formal methods courses. Instructors must model the practice by writing specs for their own assignments, demonstrating that the skill is as essential as writing loops.

Mathematics—predicate logic and elementary set theory—offers a natural medium for informal specifications. Unfortunately, many programmers find even this modest math intimidating, a cultural artifact of education systems that present mathematics as abstract and disconnected from software.

The Blueprint Metaphor Revisited

While blueprints are visual, specifications need not be pictures. Diagrams can aid understanding for simple cases, but they often hide complexity rather than expose it. Flowcharts, once popular, fell out of favor for precisely this reason. A well‑crafted textual spec, possibly augmented with concise mathematical notation, remains the most reliable guide.

Concluding Thoughts

Specification is not a silver bullet; it will not eliminate every bug, nor can it compensate for incorrect requirements. However, neglecting it guarantees a higher likelihood of design errors slipping into code. By committing to the discipline of writing what a program does—and, when necessary, how it does it—developers gain:

• Clear documentation that travels with the code.
• Early detection of subtle design flaws.
• Confidence to experiment with performance optimizations, knowing that a formal check backs the changes.

In the end, the choice is simple: either begin each project with a thoughtful blueprint, or accept that every line of code will be a patch built on an uncertain foundation.

---

For further reading on formal verification tools, see the TLA+ homepage (https://lamport.azurewebsites.net/tla/tla.html).