Lamport Demands Math Specs as Amazon and Xbox Tap TLA+ to Stop Crashes
Microsoft Research
Software engineers who code without writing specifications deceive themselves about thinking, ensuring that every line they produce starts its life as an unmaintainable patch.
AI-assisted summary of Leslie Lamport: Thinking Above the Code — original source. Check the original for full context.
Source published:
Key ideas
- Leslie Lamport advocates that software developers adopt the discipline of architects by writing specifications before coding, emphasizing that thinking without writing is merely pretending to think. (2:10)
- Formal specification methods like TLA+ have delivered substantial industrial impact, including preventing critical outages at Amazon Web Services and uncovering a hardware bug in the Xbox 360 memory architecture that would have caused crashes after four hours. (20:40)
- The vast majority of software execution can be modeled using standard behavioral state machines composed of an initial state predicate and a next-state relation, without needing complex temporal logic for safety properties. (14:18)
- Lamport strongly rejects industry practices like 'specification by example' and testing as substitutes for formal specifications, noting that examples obscure edge cases and third-party library reuse routinely fails when behavioral specs are missing. (52:15)
Detailed notes
## Background Published by Microsoft Research on YouTube on July 15, 2014, this video captures Leslie Lamport's plenary address at the Microsoft Faculty Summit. According to the page description, while architects draw detailed blueprints before building, software engineers rarely do; Lamport explains why writing specifications—the software equivalent of blueprints—is vital before coding, especially for complex, concurrent, and distributed systems.
## TL;DR Turing Award laureate Leslie Lamport argues that software development suffers because engineers rush into code without first thinking through their designs on paper. He introduces a continuum of specifications ranging from brief prose to rigorous mathematical formulations like TLA+, demonstrating how state machines and basic mathematical concepts cleanly describe systems without the distorting biases of programming languages. Drawing on concrete examples like non-recursive Quicksort, text pretty-printing, and industry deployments at Amazon Web Services and the Xbox 360, Lamport illustrates that specifying safety properties prevents severe architectural bugs that code testing misses. Ultimately, he contends that writing is the only dependable mechanism for clear thinking, urging developers to treat coding as an implementation detail downstream of architectural design.
## Atmosphere & style The lecture carries an energetic, intellectually demanding, and delightfully irreverent tone, propelled by Lamport's dry wit and no-nonsense delivery. Standing before an audience of computer science academics and researchers, he punctures conventional software engineering dogma with sharp aphorisms, humorously dismissing trendy methodologies while maintaining an infectious passion for mathematical elegance. The experience feels like an uncompromising masterclass from a legendary pioneer who effortlessly demystifies formal methods, alternating between warm humor and unapologetic, candid critiques of lazy programming habits.
## Bulletin - [02:10](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=130s) Leslie Lamport advocates that software developers adopt the discipline of architects by writing specifications before coding, emphasizing that thinking without writing is merely pretending to think. - [20:40](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=1240s) Formal specification methods like TLA+ have delivered substantial industrial impact, including preventing critical outages at Amazon Web Services and uncovering a hardware bug in the Xbox 360 memory architecture that would have caused crashes after four hours. - [14:18](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=858s) The vast majority of software execution can be modeled using standard behavioral state machines composed of an initial state predicate and a next-state relation, without needing complex temporal logic for safety properties. - [52:15](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=3135s) Lamport strongly rejects industry practices like 'specification by example' and testing as substitutes for formal specifications, noting that examples obscure edge cases and third-party library reuse routinely fails when behavioral specs are missing.
## Key takeaways - [02:10](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=130s) Thinking must precede coding, and writing is nature's way of revealing sloppy thinking; without writing specifications down, developers are deceiving themselves about system correctness. - [04:10](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=250s) Specifications exist along a wide continuum: short prose for everyday code, mathematical prose for subtle behaviors, and formal languages for mission-critical concurrent and distributed systems. - [06:40](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=400s) Computer science should mirror the natural sciences by abstracting messy physical execution down to simple mathematical models, primarily mathematical functions and sequences of states. - [08:28](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=508s) Mathematical functions specify input-output transformations but cannot capture execution mechanics, algorithmic differences, or reactive, non-terminating systems like operating systems. - [11:15](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=675s) In the standard behavioral model, execution is represented as a sequence of states, where state transitions are governed by an initial state predicate and a next-state relation operating on unprimed and primed variables. - [13:04](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=784s) System properties split into safety ('nothing bad happens', verifiable at a finite state) and liveness ('something good eventually happens', verifiable only over infinite behaviors), with safety being where the majority of subtle bugs occur. - [17:29](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=1049s) Non-determinism does not require esoteric mechanics; it simply means that a single state allows multiple valid assignments of values to the next-state primed variables. - [20:40](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=1240s) Real-world engineering at Amazon and Microsoft demonstrates that formal specifications in TLA+ catch critical concurrency bugs that evade test suites and give teams confidence to make aggressive performance optimizations. - [25:08](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=1508s) Informal specifications written in mathematical prose are essential when requirements are subjective or unsuited to automated formal verification, as demonstrated in the design of the TLATeX pretty-printer. - [34:49](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=2089s) Thinking at the code level traps programmers in implementation details, such as treating recursion as an intrinsic part of Quicksort rather than modeling it abstractly as non-deterministic transitions over a set of remaining intervals. - [40:51](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=2451s) PlusCal allows developers to express algorithms in familiar pseudocode syntax while leveraging arbitrary mathematical expressions and compiling directly to TLA+ for model checking and formal verification. - [40:51](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=2451s) Model checkers like TLC are indispensable for concurrent and distributed systems because human intuition alone cannot reliably master complex concurrent interactions. - [48:03](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=2883s) Every piece of code written without an upfront specification starts its life as a patch, compounding technical debt and making maintenance progressively more difficult. - [52:15](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=3135s) Specification by example and test-driven development are inadequate substitutes for formal specifications because concrete examples restrict attention to happy paths while obscuring rare, critical edge cases. - [55:17](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=3317s) Modern code reuse frequently fails in practice because libraries lack rigorous specifications describing what they do, forcing engineers to spend excessive time reverse-engineering internal behaviors. - [57:12](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=3432s) TLA+ isolates the complexity of temporal logic almost entirely: roughly 999 lines of a 1,000-line specification are standard discrete mathematics defining safety, with temporal logic reserved solely for the final liveness formula.
## Detailed walkthrough ### [00:01](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=1s) Introduction by Judith Bishop
Judith Bishop welcomes attendees back to the plenary session of the Microsoft Faculty Summit to introduce Leslie Lamport, Principal Researcher at Microsoft Research Silicon Valley and recipient of the A.M. Turing Award. Bishop underscores the pervasive impact of Lamport's foundational contributions on modern computing: from students and faculty teaching operating systems courses to anyone interacting with modern computers. His seminal concepts—such as logical clocks, safety and liveness, and sequential consistency—provided the theoretical bedrock that allowed computing systems to transition safely from isolated desktop machines to vast networks of interconnected devices.
Bishop outlines Lamport's storied career across elite institutions and research organizations, including MIT, Brandeis University, Digital Equipment Corporation (DEC), Compaq, and SRI International. Beyond his core computer science research, Lamport has received multiple honorary doctorates and sought to reveal aesthetic elegance to technical practitioners. He created LaTeX to help scientists see the inherent beauty in their written work; now, Bishop notes, he is on a mission to convince software engineers that another discipline holds comparable beauty: mathematics.
[02:10](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=130s) Why, When, and How to Think
Taking the podium, Leslie Lamport begins by framing the central question of his lecture: *“Thinking above the code: why do we think?”* Thinking serves as humanity's primary tool for tackling high-stakes challenges, whether hunting a saber-toothed tiger, constructing a house, or writing a computer program. However, the timing of thought is critical. When hunting a saber-toothed tiger, one must think before stepping outside the cave, because “when the tiger is charging at you, it's a little late.” Similarly, house construction demands that the design be settled before ground is broken; one should never begin figuring out the structure while carpenters are actively nailing down the roof. Applying this principle directly to software development, Lamport argues that developers must think thoroughly before writing a single line of code.
Lamport highlights the disciplined mechanism needed to make thinking effective, referencing cartoonist Richard Guindon: “Writing is nature's way of letting you know how sloppy your thinking is.” Lamport warns against internal mental simulations, asserting that anyone attempting to reason through complex systems without writing is almost certainly deceiving themselves:
> “If you're thinking without writing, chances are you're fooling yourself, we're only pretending to think.”
- **The saber-toothed tiger dilemma:** Prehistoric hunters could not write because writing had not yet been invented, rendering the activity exceptionally dangerous. - **The builder's prerequisite:** Builders draft visual designs prior to physical construction; these architectural drawings are called blueprints. - **The programmer's equivalent:** Software blueprints exist under a different name: *specifications*.
[04:10](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=250s) The Spectrum of Specifications
The moment the word "specification" is uttered, Lamport observes, software engineers reflexively panic at the prospect of indecipherable formal notation, complex mathematical symbols, and rigid academic overhead. But just as construction blueprints span an entire spectrum—from quick, hand-drawn weekend project sketches, to standard municipal house plans, to massive multi-sheet architectural blueprints for skyscrapers—software blueprints exist across a wide continuum. Lamport emphasizes that specifications do not follow a one-size-fits-all methodology, categorizing them into three primary tiers:
1. **Short Prose Specifications:** Suitable for the vast majority of ordinary code. A few straightforward sentences suffice to document intent and structure. 2. **Mathematical Prose:** Required when code exhibits subtle or tricky behavior. It relies on standard natural language prose, but with rigorous mathematical precision. 3. **Formal Specifications:** Essential for systems that are deeply complex, subtle, or mission-critical, particularly concurrent and distributed systems.
When dealing with mission-critical concurrency, engineers must employ software tools to verify that their architectural designs are sound. Lamport underscores that this verification step strictly dictates the notation used: “If you're going to use tools, it means you need a formal language, because tools don't understand prose.”
[06:40](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=400s) Modeling Reality: From Astronomy to Computer Science
Writing a specification requires clear thinking, and Lamport argues that software engineers should adopt the cognitive framework of computer scientists—that is, the scientific method itself. The defining achievement of science is constructing simple mathematical models to describe complex physical realities. Astronomy serves as the premier historical example: while an actual planet possesses turbulent weather systems, shifting oceans, mountains, and gravitational tides, celestial mechanics made immense strides by abstracting all of those physical intricacies away, modeling each planet simply as a point mass characterized solely by its position and momentum.
```mermaid flowchart TD accTitle: Scientific Modeling in Astronomy and Computing accDescr: Comparison showing how physical reality is abstracted into mathematical models in astronomy and computing.
subgraph Astronomy["Astronomy"] A1["Physical Planet<br/>(Oceans, tides, mountains, weather)"] -->|"Abstracted to"| A2["Mathematical Point Mass<br/>(Position & Momentum)"] end
subgraph Computing["Computer Science"] C1["Digital Hardware & Execution<br/>(Chips, consoles, executing programs)"] -->|"Abstracted to"| C2["Mathematical Models<br/>(Functions & Behavioral Sequences)"] end ```
In computer science, reality consists of physical digital artifacts: processor chips, gaming consoles, or physical computers executing instructions. To reason about these digital realities cleanly, engineers must use formal mathematical models. While theoretical computer science contains many abstract structures—such as Turing machines and partially ordered sets of events—Lamport singles out two models as uniquely foundational and practical: - **Functions** - **Sequences of States**
[08:28](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=508s) The Function Model and Its Limitations
The simplest model for a program is a mathematical function that maps an input (or set of inputs) to an output. Lamport points out that a mathematical function is far simpler than a programming language "function" or procedure. In pure mathematics, a function is strictly defined as a set of ordered pairs. For instance, the function that squares natural numbers is the infinite set of pairs `{(0, 0), (1, 1), (2, 4),...}`. Writing `square(2) = 4` simply states that the ordered pair `(2, 4)` is an element of that set. To specify any function, one defines two aspects: 1. The **domain** (the set of all first elements in the pairs, such as the natural numbers, denoted as `Nat`). 2. The mapping rule for every value $x$ in that domain (mapping $x$ to $x^2$).
Lamport humorously distances himself from language design intricacies: “I'm not a programming language expert, so I don't know what those things that programming languages call functions are, but I know what math is, and math is a lot simpler.”
Despite its clarity, the functional model suffers from two major limitations: - **It omits operational behavior:** A function specifies *what* a program computes, never *how* it computes it. Quicksort and Bubblesort compute identical input-output functions, yet represent completely different algorithms. - **It cannot model reactive or non-terminating systems:** Systems such as operating systems never terminate to yield a final output pair; they run indefinitely (or until the sun explodes). A non-terminating system cannot be modeled as an input-to-output mapping.
[11:15](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=675s) The Standard Behavioral Model and Euclid’s Algorithm
To specify systems that execute over time or run indefinitely, Lamport turns to the **standard behavioral model**. Within this framework: - A **state** is defined as an assignment of values to variables. - A **behavior** is an execution modeled as a sequence of states. - A **program** is modeled as the set of all its possible behaviors (every valid execution sequence).
To illustrate this with an algorithm (which Lamport characterizes as simply an “abstract program”), he examines Euclid's algorithm for finding the greatest common divisor (GCD) of two integers, $m$ and $n$. The algorithm initializes variable $x$ to $m$ and $y$ to $n$, continually subtracts the smaller value from the larger, and terminates when $x = y$, at which point both variables hold the GCD.
Given inputs $m = 12$ and $n = 18$, the algorithm yields a deterministic behavior consisting of a single sequence of three states:
| Step | State Assignment | Transition Action | |:--- |:--- |:--- | | **Initial State** | $x = 12,\; y = 18$ | Subtract smaller ($x$) from larger ($y$): $18 - 12 = 6$ | | **Second State** | $x = 12,\; y = 6$ | Subtract smaller ($y$) from larger ($x$): $12 - 6 = 6$ | | **Final State** | $x = 6,\; y = 6$ | $x = y$; algorithm stops with $\gcd(12, 18) = 6$ |
[13:04](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=784s) Safety and Liveness Properties
Lamport addresses how to formally describe arbitrary sets of behaviors. He cites a fundamental theorem: any set of behaviors $B$ can be expressed as the intersection (conjunction) of two distinct properties: a **safety property** and a **liveness property**.
Without getting bogged down in overly formal mechanics, Lamport provides the operational intuition that distinguishes them: - **Safety Properties:** A safety property is violated if and only if it fails at a specific, identifiable point in time during the execution behavior. Lamport points to partial correctness as a quintessential safety property: if a program finishes its execution and outputs an incorrect result, you can pinpoint the exact moment of failure—namely, the state where the program terminated with the wrong value. - **Liveness Properties:** A liveness property asserts that something good must eventually occur. Unlike safety, a liveness property cannot be declared violated at any finite step; you must observe the complete, infinite behavior to determine whether it failed. Lamport identifies termination as the classic liveness property: at any finite moment during execution, one cannot assert that the program will never terminate, because it might still terminate in a subsequent step.
[14:18](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=858s) Specifying Safety Properties with Mathematics
A set of behaviors cannot generally be evaluated simply by inspecting a finite snippet of execution; for instance, determining that a system never terminates requires looking across its entire behavior. Behaviors are fundamentally specified using two distinct types of properties: safety and liveness. In practice, safety is far more critical because that is where errors are most likely to lurk and where bugs tend to be much more subtle. For the sake of time, Leslie Lamport sets liveness aside to focus exclusively on safety properties.
Specifying a safety property requires exactly two ingredients: the set of possible initial states, and a next-state relation that describes all admissible successor states from any given state. When considering what language should express these foundations, Lamport advises acting like scientists, pointing out that the universal language of science is mathematics.
```mermaid flowchart TD accTitle: Safety Property Specification accDescr: Diagram showing how an initial predicate and next-state relation generate state transitions. subgraph Spec["Safety Specification"] Init["Initial Predicate: Init"] Next["Next-State Relation: Next"] end subgraph Execution["Execution Behavior"] S0["State 0: (x, y)"] S1["State 1: (x', y')"] S2["State 2: (x'', y'')"] end Init --> S0 S0 -->|"Next(x, y, x', y')"| S1 S1 -->|"Next(x', y', x'', y'')"| S2 ```
In mathematical specifications, both components are written as formulas. Unprimed variables denote values in the current state, while primed variables denote values in the successor state. Lamport illustrates this using Euclid’s algorithm: - The initial state predicate: $x = m \land y = n$. Only a single initial state satisfies this relation once the parameters $m$ and $n$ are chosen. - The next-state relation: a disjunction handling the two algorithmic branches: $$(x > y \land x' = x - y \land y' = y) \lor (y > x \land y' = y - x \land x' = x)$$ - “Now in practice specifying safety just turns out to be more important because that's where errors are most likely to occur and tend to be more subtle,” Lamport notes.
[17:29](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=1049s) Tracing Euclid's Algorithm and Understanding Non-Determinism
To demonstrate how formal formulas generate actual executions, Lamport walks through a concrete evaluation of Euclid's algorithm with concrete values: $m = 12$ and $n = 18$. Substituting these into the initial state predicate yields the single starting pair $x = 12$ and $y = 18$. The next state is then computed by plugging these values into the next-state formula:
| Step | Current State ($x, y$) | Next-State Evaluation | Next State ($x', y'$) | Action | |:--- |:--- |:--- |:--- |:--- | | **0** | $x = 12, y = 18$ | $12 > 18$ is false; $18 > 12$ is true. Formula simplifies to $x' = 12 \land y' = 18 - 12$. | $x = 12, y = 6$ | Step 1 | | **1** | $x = 12, y = 6$ | $6 > 12$ is false; $12 > 6$ is true. Formula simplifies to $x' = 12 - 6 \land y' = 6$. | $x = 6, y = 6$ | Step 2 | | **2** | $x = 6, y = 6$ | Both $6 > 6$ guards evaluate to false. Entire next-state relation becomes false. | None | Halts |
Because no possible values of $x'$ and $y'$ can satisfy the relation when $x = y = 6$, there is no next state, which signifies mathematically that the program has cleanly terminated.
Lamport highlights that Euclid’s algorithm is strictly deterministic because for every state $(x, y)$, there is at most one pair of successor values $(x', y')$ that makes the next-state relation true. Modeling non-determinism does not require any special or esoteric mechanics; it simply means having a next-state relation where a single current state allows multiple valid assignments to the primed variables. “Multiple assignments of values to primed variables that make next true for a single assignment of values to unprimed variables—that's what non-determinism is all about,” Lamport clarifies, demystifying the concept.
[20:40](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=1240s) Formalizing in TLA+ and Industrial Impact at Amazon and Xbox
Formal languages exist primarily because tools require them. While mathematicians historically relied on informal mathematical notation, running an automated solver like Mathematica demands conforming to its precise syntax. Similarly, to check models or verify proofs mechanically, Lamport introduces TLA+. In TLA+, the mathematical definition of Euclid's algorithm is wrapped inside a module (`MODULE Euclid`) with explicit declarations: declaring $m$ and $n$ as constants, declaring $x$ and $y$ as variables, and importing arithmetic operators by extending the standard `Integers` module.
```mermaid flowchart LR accTitle: TLA+ Tooling Ecosystem accDescr: Flow from a TLA+ specification to model checking or mechanical proof verification. Spec["TLA+ Specification"] Spec -->|"Instantiate Constants"| TLC["TLC Model Checker"] TLC --> Check["Exhaustive State Exploration"] Spec -->|"Write Proofs"| TLAPS["TLA+ Proof System"] TLAPS --> Verified["Mechanically Checked Correctness"] ```
TLA+ allows users to exhaustively model check all possible executions of a design on small instances in a matter of nanoseconds, or to write formal proofs that are verified mechanically by a theorem prover. Lamport mocks the prevailing software engineering prejudice that “math works only for toy examples” and that modeling “real” systems requires programming constructs like types, procedures, and object-oriented abstractions, flatly answering: “Wrong.”
To dispel that myth, Lamport shares real-world evidence from industry adoption: - **Amazon Web Services (AWS)**: Lamport quotes Amazon engineer Chris Newcomb: “We have used TLA+ on 10 large complex real-world systems. In every case, TLA+ has added significant value, either preventing subtle serious bugs from reaching production or giving us enough understanding and confidence to make aggressive performance optimizations without sacrificing correctness.” Lamport underscores that contrary to claims that formal methods destroy performance or that management will forbid them, Amazon managers actively allocate engineering time during annual planning to write TLA+ specifications. - **Xbox 360 Memory System**: Microsoft researcher Chuck Thacker had an intern write a TLA+ specification of the Xbox 360 cache coherence and memory system. Merely writing down the formal specification—without even running the model checker—surfaced a subtle concurrency bug. When presented with it, the memory system’s architects at IBM acknowledged that the bug had completely eluded their hardware test suites and would have caused every single Xbox 360 console in the world to crash after approximately four hours of operation.
[25:08](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=1508s) The Limits of Formalization: Informal Specs and TLATeX
While TLA+ is extraordinarily potent, Lamport emphasizes that today's talk is not about TLA+ itself, but about the necessity of *informal* specifications. To illustrate why informal specifications are indispensable, he turns to `TLATeX`, the pretty-printer tool he built for typesetting TLA+ formulas into LaTeX.
```mermaid flowchart TD accTitle: Pretty-Printer Decision Process accDescr: How TLATeX must infer user intent for formula alignment. Input["ASCII Input Formula"] Heuristic{"Align symbols or keep naive flow?"} Input --> Heuristic Heuristic -->|"User intended alignment"| Pretty["Aligned Mathematical Formatting"] Heuristic -->|"Alignment was accidental"| Naive["Naive Linear Output"] Pretty --> Subjective["Correctness = What the user wanted"] Naive --> Subjective ```
When pretty-printing mathematical text, a naive translation simply replaces ASCII tokens (such as `/\` with $\land$). However, alignment carries syntactic and semantic weight in TLA+: - If a user writes an indented list of conjunctions and alignment between equality signs, they almost certainly intended for those operators to line up neatly in the typeset output. - Conversely, in other formulas, identical vertical column alignments may be purely coincidental, and forcing an aligned tabular layout would distort the author's visual intent into an ugly, unintended layout.
The fundamental dilemma is that there is no rigorous mathematical definition for what constitutes "correct" aesthetic alignment; correctness is entirely subjective and boils down to whatever the user wanted. Because human desires cannot be captured in a rigorous mathematical formula, it is impossible to write a formal correctness specification for such a program. Yet Lamport firmly rejects the excuse that an absence of formal rules justifies jumping straight into code without design: “Not knowing what a program should do doesn't mean you don't have to think, you just go to code—it means you have to think a lot harder.” When requirements are messy, subjective, and undefined, writing an informal specification is more vital than ever.
[27:19](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=1639s) Specifying a Pretty-Printer: Six Rules in Mathematical Prose
Faced with the challenge of formatting text where it is initially unclear what the formatting even ought to look like, Leslie Lamport explains that writing is an indispensable tool for thinking. To design his pretty-printer, he wrote a specification consisting of just six rules and accompanying definitions written as informal mathematical prose inside comments. Reading one of the rules aloud—“a left comment token is left comment aligned with its covering token”—Lamport admits with a laugh that he no longer remembers what it means without checking the spec, yet terms like “left comment aligned” and “covering token” were mathematically defined concepts. Formulating the system this way paid off immediately: it proved far easier to understand and debug six high-level rules through examples and dedicated debugging instrumentation than to debug 850 lines of code (which likely would have ballooned even further without the specification).
Lamport addresses why he chose informal mathematical prose rather than a formal TLA+ specification for the pretty-printer. First, the stakes were low: the world will not collapse if a comment is slightly misaligned in a pretty-printer, and formatting inherently lacks absolute corner-case perfection. Second, formal tooling like model checkers would not have been useful because there were no crisp invariant properties to verify against. This example illustrates what is typical of specifications: it sits at a higher level of abstraction than the code, it can be implemented in any programming language, and no popular programming methodology would have helped write it or eliminated the need for it. As Lamport emphasizes: “You write a spec to help you think about the problem before you think about the code.”
Conversely, what made this pretty-printer spec atypical is that it is unusually subtle—since 95% of everyday code requires far less thought—and it was expressed as an axiomatic set of rules. A set of rules or axioms is generally a poor choice for a specification because rule interactions are notoriously difficult to understand, but it happened to fit this problem well. Lamport draws a fundamental contrast between problem types: “Specifying what the pretty printer should do is hard; implementing the spec was easy. Specifying what a sorting program should do is easy; figuring out how to implement it efficiently is hard, at least if nobody has showed you how.”
- The pretty-printer specification comprised six core rules plus definitions written in comments as informal mathematical prose. - Designing the rules first kept the implementation down to approximately 850 lines of code. - Formal TLA+ and model checking were skipped because total correctness across every corner case was non-critical and no automated checker could evaluate aesthetic layout choices. - Standard programming methodologies offer no assistance in conceptualizing high-level domain rules prior to coding.
[32:03](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=1923s) Quicksort and the Trap of Pseudocode
To illustrate how specifications guide algorithms that are difficult to implement efficiently, Lamport turns to Tony Hoare's Quicksort. Designed as a divide-and-conquer algorithm to sort an array $A[0 \dots n-1]$ of numbers, Quicksort relies on a partition procedure. Given bounds `low` and `high`, the partition procedure selects a pivot index in the range $\text{low} \dots \text{high}-1$ and permutes the sub-array so that every element up to the pivot is less than or equal to every element from the pivot plus one upward. While the clever internal mechanics of partitioning represent the real trick of Quicksort, Lamport abstracts that step away to focus entirely on the overall control structure.
```mermaid flowchart TD accTitle: Recursive Quicksort Flow accDescr: Standard divide-and-conquer recursion tree for quicksort down to base cases.
subgraph RecursiveCall["Recursive Step: qs(low, high)"] Cond{"low < high?"} Part["pivot = partition(low, high)"] Left["qs(low, pivot)"] Right["qs(pivot + 1, high)"] Done["Done (single element)"] end
Cond -- "Yes" --> Part Part --> Left Part --> Right Cond -- "No" --> Done ```
When written in standard pseudocode, Quicksort defines a recursive procedure `qs(low, high)`: if `low < high`, it invokes `partition(low, high)` and then recursively invokes `qs` on the two resulting sub-intervals; if not, it terminates. The main program simply calls `qs(0, n - 1)`. Lamport acknowledges that this informal pseudocode is perfectly easy to understand and straightforward to translate into almost any programming language. However, he warns that it hides a fundamental conceptual flaw: “Recursion is not a fundamental part of quicksort; it's just one way of implementing divide and conquer.”
- Quicksort partitions an array $A[0 \dots n-1]$ around a chosen pivot point between `low` and $\text{high}-1$. - Pseudocode specifications rely heavily on recursive procedure calls and base-case checks. - Recursive formulations obscure alternative execution models, particularly when attempting to parallelize across multiple CPU cores.
[34:49](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=2089s) Thinking Above the Code: A Non-Recursive Quicksort in Math and TLA+
Lamport poses a classic challenge: ask programmers or colleagues to write a non-recursive version of Quicksort, and almost nobody can produce a working solution in ten minutes standing on their feet. Because their thinking is trapped inside code, they immediately attempt to manually compile the recursion by simulating a call stack. The true mathematical solution, however, is simple: maintain a set $U$ of index ranges that still require partitioning, initialized to contain the single pair representing the full range, $\{ (0, n-1) \}$. Described as a state machine with an `Init` predicate and a `Next` relation, $A$ is initially any array of numbers of length $n$, and $U = \{ (0, n - 1) \}$.
```mermaid flowchart LR accTitle: Set-Based Iterative Quicksort Transition accDescr: State transition relation showing removal of an interval from set U and addition of sub-intervals.
subgraph StateUpdate["Next-State Relation"] U_Old["U contains (B, T)"] Check{"B = T?"} BranchWork["Pick pivot P<br/>Permute A to A'<br/>U' = (U \ {(B, T)}) ∪ {(B, P), (P+1, T)}"] BranchBase["A' = A<br/>U' = U \ {(B, T)}"] end
U_Old --> Check Check -- "B ≠ T" --> BranchWork Check -- "B = T" --> BranchBase ```
The next-state relation specifies transitions between current values $(A, U)$ and next values $(A', U')$. As long as $U \neq \emptyset$, the algorithm non-deterministically selects any pair $(B, T) \in U$. If $B \neq T$, it picks a pivot index $P \in [B, T - 1]$, updates $A'$ to any valid permutation yielded by partitioning within those bounds, and updates $U'$ by removing $(B, T)$ and adding the two sub-intervals $(B, P)$ and $(P + 1, T)$. If $B = T$, no sorting is needed: $A'$ remains unchanged and $(B, T)$ is simply excised from $U$. Lamport underscores why this formulation is superior: “Why can almost no one find this version of quicksort? Because people's minds are stuck in code; they haven't learned to think at a higher level than the code.”
This mathematical specification is substantially more general than the textbook recursive algorithm: the execution traces generated by recursive Quicksort represent merely a strict subset of the valid behaviors allowed by this set-based specification. Because picking arbitrary elements translates directly into existential quantification ($\exists$) and state updates map to set operations, the entire algorithm can be expressed cleanly as a formal TLA+ formula. For engineers who prefer an algorithmic presentation over pure formulas, Lamport introduces PlusCal. PlusCal appears syntactically like a toy programming language embedded inside comments of a TLA+ module, but because any expression within it can be an arbitrary mathematical TLA+ expression, it provides vastly greater expressive power than ordinary programming languages.
- Iterative Quicksort maintains an outstanding work set $U$ containing interval pairs $(B, T)$. - The initial state relation defines $A$ as an array of length $n$ and $U = \{ (0, n - 1) \}$. - The next-state relation $Next$ operates non-deterministically on any element in $U$ until $U = \emptyset$. - The recursive version is merely one specific execution schedule among many valid behaviors permitted by the set-based specification. - PlusCal embeds algorithmic control structures inside TLA+ modules while allowing full mathematical expressions within statements.
[40:51](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=2451s) PlusCal, TLA+, and the Need for Model Checkers in Concurrent Systems
Lamport reflects on the expressive power of PlusCal, explaining that it compiles cleanly into an easy-to-understand TLA+ specification. In his own workflow, he regularly writes algorithms in PlusCal, but when it comes time to verify their correctness, he reasons directly about the resulting TLA+ translation using formal tools like the TLC model checker and the TLA+ proof system. He shifts the discussion from simple programs that compute a finite mathematical function to programs that run forever—such as operating systems and distributed systems.
These long-running systems inherently involve concurrency, an area where human intuition routinely fails. Lamport candidly admits his own limitations when tackling them unaided: “Few people can get them right by just thinking and writing; I'm not one of them.” Because human reasoning alone cannot reliably master concurrent interactions, automated verification tools become non-negotiable. He points out that the TLC model checker was the decisive reason TLA+ proved so immensely valuable to engineers at Amazon. For any concurrent or distributed algorithm, writing a specification and thoroughly model checking it is essential to achieving correctness.
```mermaid flowchart TD accTitle: Workflow from PlusCal to Verified Implementation accDescr: An algorithm is written in PlusCal, translated to TLA+, verified via model checking and proofs, and then implemented.
subgraph SpecPhase ["Specification and Verification"] PC["PlusCal Algorithm"] --> Trans["TLA+ Translation"] Trans --> Tools["TLA+ Tools:<br/>Model Checker (TLC) & Theorem Prover"] end
subgraph CodePhase ["Implementation"] Tools --> Impl["Implementation Code<br/>(Operating & Distributed Systems)"] end ```
- Programs that run indefinitely almost always involve concurrency and distributed components. - Amazon Web Services engineers successfully leveraged the TLA+ model checker to uncover subtle bugs in critical distributed systems. - PlusCal provides an algorithmic syntax resembling pseudocode, while translating into pure TLA+ for formal verification.
[42:14](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=2534s) The Discipline of Thinking: Writing Down What Code Does
Turning to the other 95% of software engineering—the seemingly straightforward code—Lamport shares a concrete example from his own programming. He wrote a specification for a module simply to confirm he truly understood what the code had to do before typing out a single line of implementation. Without writing it down, one only assumes the behavior is obvious. Committing it to a specification forced him to confirm that it was genuinely as simple as he imagined. Furthermore, writing it paid off later: whenever he needed to interact with that module down the road, he did not need to decipher the underlying code; he merely read the concise specification.
From this experience, Lamport extracts a fundamental rule for software specifications: a specification describing what a piece of code does should articulate everything anyone needs to know in order to use that code. In his example, the internal mechanism was too trivial to warrant an elaborate internal spec. Had it turned out to be unexpectedly intricate during coding, he would have halted coding immediately and returned to writing a spec. He challenges the audience on human nature and problem-solving: “Everyone thinks they think, but if you don't write down your thoughts, you're fooling yourself.” To think before you code fundamentally means to write before you code, because a specification is simply what you write before coding.
- Any code that another person—or the original author a month later—might need to use or modify warrants a specification. - A specification can cover an entire architecture, a subsystem, a single class, a method, or even a tricky algorithm nested inside a method. - Specifications must document *what* the code does (interfaces, preconditions, outputs), and should detail *how* it does it only when the underlying algorithm is subtle and complex.
[44:50](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=2690s) Mathematical Thinking, Comments, and the Separation of Coding
Lamport argues that programmers must learn to view their systems above the code level, expressing designs in terms of discrete states and behaviors, or mathematical functions mapping inputs to outputs. Regardless of whether a specification is written in formal mathematical syntax, informal prose, or high-level pseudocode, the underlying thought process must remain mathematical. When asked how one learns this art, Lamport insists that the most effective route to writing good informal specifications is learning to write formal ones first. Just as a programmer learns to code by writing programs, running them, and fixing bugs, one learns to specify by writing formal specs, running them against a model checker, and correcting the errors that the tool exposes.
While TLA+ may not be the optimal formal language for every domain, Lamport maintains it is uniquely effective for teaching engineers how to think mathematically. Once a specification exists, it must be connected to the codebase. This bridge belongs directly in the program comments, mapping mathematical abstractions to concrete data structures—for instance, noting that a mathematical graph is realized as an array of node objects and an array of link objects. Lamport stresses that he has no dogma regarding programming languages, frameworks, or coding methodologies: “Writing a spec isn't going to catch coding errors because it's not about coding; it'll catch algorithm errors.” Coding remains a separate discipline where testing and debugging are still necessary, but an upfront specification prevents foundational design flaws and makes programs vastly superior.
- Formal specs build the intellectual rigor needed to write clear, unambiguous informal specifications. - Model checkers provide immediate feedback on specifications analogous to compilers and test suites for source code. - Specs and the explicit mapping of mathematical concepts to implementation variables should live inside the source code comments. - Upfront specifications do not replace unit testing or debugging, but they eliminate algorithmic mistakes before code is ever written.
[48:03](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=2883s) Why Writing Is Hard, the Reality of Patches, and Eisenhower's Lesson
Programmers frequently resist writing specifications because writing is intellectually demanding. Lamport observes that writing is hard precisely because thinking is hard, humorously paraphrasing the ancient maxim often attributed to Archimedes or Euclid that there is no royal road to mathematics. Writing acts like running: if you do not practice, your writing muscles atrophy, making it tempting to find excuses to avoid it altogether. The most pervasive excuse is the certainty of change: requirements shift, features are added, specifications contain flaws, and code inevitably diverges from the original plan. In the real world, programs are patched rather than redesigned from scratch.
Even so, Lamport insists that writing an upfront specification is vital for two reasons. First, anyone tasked with maintaining the codebase later—often the original author—will be deeply grateful for every word and formula left behind. Second, patching code degrades it: “Every time code is patched, it becomes a little uglier, harder to understand, and harder to maintain; and if you don't start with a spec, every piece of code you write is a patch.” Without a baseline design, software starts its life as an ugly patch on day one. Invoking Dwight D. Eisenhower's famous military dictum—that no battle was ever won according to plan, but no battle was ever won without one—Lamport cautions the audience against those who dismiss specifications: “Thinking doesn't guarantee that you won't make mistakes, but not thinking generally guarantees that you will.”
- Useful programs inevitably attract users whose evolving requirements force patches and modifications. - When modifications occur, programmers should strive to update the specification alongside the code. - Starting without an explicit specification ensures the codebase is disorganized and difficult to maintain from inception. - Lamport directs interested practitioners to his Microsoft Research homepage for links, documentation, and tools related to TLA+.
[52:15](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=3135s) Q&A: Specification by Example and Test-Driven Development
Following the presentation, Lamport opens the floor to a brief question-and-answer session. An audience member raises a question about pragmatic industry trends, asking Lamport for his view on "specification by example," an approach closely tied to test-driven development (TDD) where concrete usage examples serve as the functional specification under the justification that formal completeness is undecidable anyway.
Lamport rejects the premise outright, calling specification by example a "terrible pragmatic approach." While he readily concedes that concrete examples are wonderful pedagogical tools for explaining a concept to a human being, he argues that relying on them as a specification actively prevents genuine engineering analysis. Concrete examples confine the developer's mindset to convenient scenarios. The central challenge of programming, Lamport argues, is not designing for the obvious, straightforward cases, but anticipating and correctly handling the rare, difficult edge cases where systems break down.
[53:19](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=3199s) The Failure of Specification by Example
Leslie Lamport wraps up his critique of relying on code examples in place of precise specifications by sharing his personal frustrations with Eclipse plugin development. He explains that countless methods in Eclipse are documented merely with an example of code calling them. In his experience, attempting to adapt those methods to do what he actually wants almost never succeeds because the code only works for the narrow, cherry-picked scenario demonstrated in the documentation. Lamport emphasizes that while he cannot speak definitively on the viability of programming by example, substituting examples for genuine specifications fundamentally fails to communicate what a system does. As he dryly summarizes: “Programming by example I don't know about you know if that works, but specification by example, it doesn't.”
[54:09](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=3249s) Patching Code and Preserving Old Specifications
An audience member asks what engineers should do with older specifications once a bug is patched in the code, questioning whether it is useful to retain historical context or if old specs should simply be discarded. Lamport explains his own workflow, noting that whenever fixing a bug requires altering a specification, he makes sure to record detailed notes explaining exactly why the change was made, anticipating that years later he will return to the code and wonder what prompted the modification.
On the broader question of version retention, Lamport advocates strongly against throwing past documentation away, pointing out that modern digital storage makes retaining history virtually cost-free: “It doesn't cost anything to save it, so you should certainly save the old specs.” However, whether developers should explicitly document every historical change inside the text of the new specification itself remains an open design choice for which he does not claim a single definitive answer.
[55:17](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=3317s) The 95% Versus the Critical 5%: Why Undocumented Code Reuse Fails
A questioner with a PhD in formal methods challenges Lamport by observing that modern software development has moved away from formal specifications. Instead, 99% of contemporary software engineering involves copying existing algorithms and libraries, stitching them together, and tweaking them to fit immediate needs.
Lamport responds that while building software that way sounds appealing in theory, in practice it breaks down precisely because the third-party components lack rigorous specifications. Programmers end up wasting immense amounts of time reverse-engineering what external libraries actually do under the hood. While Lamport concedes that 95% of ordinary code requires very little formal specification—often just a few explanatory lines—engineers will inevitably hit a critical 5% that involves subtle concurrency or deep architectural difficulty:
> “There's gonna be something, some things, code you're gonna have to write that is subtle, it has some a bit of difficulty in it, and you want to be able to, you know, you want to be prepared for that, because we use the same techniques that you use, you know, the same lack of thought that you use when you're doing that other 95%, you're gonna screw up badly.”
[57:12](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=3432s) TLA+ and the "Evil" of Temporal Logic
An attendee asks Lamport about the theoretical foundations of his work, noting that anyone familiar with temporal logic will recognize modal concepts like future and necessity operators running beneath his presentation, and asks whether those operators could be used more directly. Lamport clarifies that TLA stands directly for the "Temporal Logic of Actions." He then offers a candid critique of the formalism, declaring: “Temporal logic is evil.” He explains that it is exceptionally hard to work with and reason about directly, yet it remains a necessary evil because it provides the best known formalism for handling liveness properties (the guarantee that something good eventually happens).
Critically, Lamport points out that safety properties (guaranteeing that nothing bad happens) are far more essential in real-world systems, and safety requires no temporal logic whatsoever. The key design breakthrough of TLA+ is that it insulates the engineer from temporal operators almost entirely:
> “The thing that makes it great is that you'll write a thousand-line specification, 999 lines are going to be ordinary math—initial predicate, next-state relation—and then the last line is going to be a temporal logic formula.”
```mermaid flowchart TD accTitle: Anatomy of a TLA+ Specification accDescr: Diagram illustrating how 999 lines of ordinary math define safety before a single line of temporal logic defines liveness.
subgraph OrdinaryMath["Ordinary Mathematics (999 Lines)"] Init["Initial Predicate (Init)"] Next["Next-State Relation (Next)"] Safety["Safety Guarantees: 'Nothing bad happens'"] Init --> Safety Next --> Safety end
subgraph TemporalLogic["Temporal Logic (1 Line)"] Live["Liveness Formula: 'Something good eventually happens'"] end
Safety -->|"Combined into spec"| TLASpec["Complete TLA+ Specification"] Live -->|"Appended at the end"| TLASpec ```
- **TLA name origin**: TLA stands for the *Temporal Logic of Actions*. - **Temporal logic usability**: Described as very difficult to use directly, but indispensable for formalizing liveness. - **Spec ratio**: In a typical 1,000-line TLA+ specification, roughly 999 lines consist of standard discrete mathematics defining initial states and state transitions, with only the final line invoking temporal logic operators.
[59:16](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=3556s) Plenary Session Conclusion
The session chair steps up to close the plenary session and thanks Lamport for his presentation. Before dismissing the attendees, the organizer delivers logistical announcements regarding evening dinner plans, instructing participants to collect their bags and board the waiting buses outside, which will transport everyone to the dinner venue and subsequently return guests to their respective hotels. The talk concludes with a round of applause for Lamport.
## Notable quotes > [48:03](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=2883s) Every time code is patched, it becomes a little uglier, harder to understand, and harder to maintain; and if you don't start with a spec, every piece of code you write is a patch. — Leslie Lamport
> [48:03](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=2883s) Thinking doesn't guarantee that you won't make mistakes, but not thinking generally guarantees that you will. — Leslie Lamport
> [02:10](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=130s) If you're thinking without writing, chances are you're fooling yourself, we're only pretending to think. — Leslie Lamport
> [27:19](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=1639s) You write a spec to help you think about the problem before you think about the code. — Leslie Lamport
> [44:50](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=2690s) Writing a spec isn't going to catch coding errors because it's not about coding; it'll catch algorithm errors. — Leslie Lamport
> [04:10](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=250s) If you're going to use tools, it means you need a formal language, because tools don't understand prose. — Leslie Lamport
> [32:03](https://www.youtube.com/watch?v=-4Yp3j_jk8Q&t=1923s) Recursion is not a fundamental part of quicksort; it's just one way of implementing divide and conquer. — Leslie Lamport
## Mentioned Amazon Web Services (AWS), Brandeis University, Chris Newcomb, Chuck Thacker, Compaq, Digital Equipment Corporation (DEC), Dwight D. Eisenhower, Eclipse, IBM, Judith Bishop, LaTeX, Leslie Lamport, Microsoft Research, MIT, PlusCal, Richard Guindon, SRI International, TLA+, TLC, Tony Hoare, Xbox 360
## Video description Architects draw detailed blueprints before a brick is laid or a nail is hammered. Programmers and software engineers seldom do. A blueprint for software is called a specification. The need for extremely rigorous specifications before coding complex or critical systems should be obvious—especially for concurrent and distributed systems. This talk explains why some sort of specification should be written for any software.
http://www.microsoftfacultysummit.com
[Source](https://www.youtube.com/watch?v=-4Yp3j_jk8Q)