Leslie Lamport's SCaLE 22x closing keynote begins with a distinction that is easy to agree with and difficult to practice: code is an implementation of an idea, while programming includes finding the right idea. The talk, delivered at an open-source conference in March 2025, is called “Coding Isn't Programming.” Its subject is not syntax, productivity tooling, or a tour of TLA+. It is the work that should happen before any of those things can help.[1][2][3]

The useful way to watch it is as a compact design procedure. First state what a computation must accomplish without smuggling in an implementation. Then describe an execution as a sequence of states connected by permitted steps. Keep only the information that can affect a future step. Finally, find a statement that remains true in every reachable state—an invariant—and use it to connect the initial condition to the promised result.

That procedure matters in open source because maintainers routinely inherit code whose intended behavior lives nowhere outside the code itself. Tests show selected executions. Types constrain selected categories of values. Review can expose a suspicious line. None of them automatically supplies the missing behavioral model. Lamport's method offers a way to write that model at the altitude where design errors are still cheap to change.

Image context: the cover is a real conference photograph of Lamport at IFIP in Udine in 2006. It predates the keynote, but it records the person whose decades of work on distributed systems and TLA+ give this apparently simple programming lesson its force.[8]

00:48–07:11 — Move the hard part above syntax

Lamport starts with concurrency because it makes the gap between an algorithm and its code impossible to ignore. Several processes can interleave their steps in many orders. A test run samples a few of those orders, often under similar timing. A synchronization bug may depend on one rare order and stay invisible until deployment. More tests can improve the sample, but they do not turn sampling into a reason that all relevant orders are safe.[1]

His response is to isolate the small piece of behavior that coordinates the system and reason about it independently of the surrounding implementation. This is abstraction in a practical sense: remove details that do not affect the question, preserve the choices that do, and make the remaining possibilities visible enough to inspect.

The important annotation is that “abstract” does not mean vague. A prose box saying “handle races correctly” has removed the code while preserving none of the behavior. A useful abstraction names what may change, what must stay fixed, and which next states are allowed. It can be much smaller than the program and more exact about the program's difficult part.

This is also why an AI code generator does not dissolve the design problem. It can translate a prompt into plausible implementation faster, but a prompt with an ambiguous result, an omitted failure case, or an inconsistent retry policy still describes the wrong system. Faster translation increases the value of deciding what is to be translated.

08:34–16:55 — Specify the result before choosing the container

The keynote's teaching example is intentionally ordinary: find the maximum element of an array. Lamport first separates the what from the how. The initial result statement seems obvious until the input is empty. Then “the largest element” names no value. That is already a design bug, even though no line of code has been written.[1][3]

This moment is more useful than the eventual loop. It shows what a specification is for: not to make familiar behavior look mathematical, but to force a decision where casual language hides one. Should an empty input be rejected? Should the result be optional? Is there a sentinel in the domain? Different APIs can make different choices. What matters is that the choice becomes part of the contract instead of an accident of initialization.

Lamport then removes another premature decision. An array supplies indices and an order, but neither matters to the mathematical result. For this problem, the input can be treated as a bag of values. That smaller view admits many implementations while excluding irrelevant obligations about positions. If stable ordering later becomes observable, the abstraction must restore it. Abstraction is therefore a claim about relevance, not a license to discard inconvenient facts.

For OSS API work, this is an excellent review question: does the issue describe the result, or has it merely proposed one implementation? “Add a cache,” “use a queue,” and “run workers in parallel” are how-statements. A what-statement says which responses may be returned, which requests may be combined or reordered, and what remains true after a crash. Once those are explicit, maintainers can compare implementations without mistaking familiarity for correctness.

17:17–26:04 — Turn the algorithm into possible next states

The middle of the talk replaces a loop listing with a state-transition view. Imagine B as the values still to examine and X as the best candidate seen so far. A step chooses a value from B, removes it, and updates X if needed. Because the choice is not fixed, this abstract algorithm represents every order in which the values could be processed. One description stands for a set of executions.[1][3]

An execution is then a sequence of states; an action relates one state to a possible successor. This is the same basic shape used by TLA+ specifications. In the common Init/Next pattern, Init characterizes allowed starting states and Next is a disjunction of allowed transitions. Primed variables denote values in the successor state.[4] The open TLA+ tool repository includes the TLC model checker that can explore such specifications, along with the parser and PlusCal translator.[5]

The viewing detail to notice is how aggressively Lamport minimizes the state. Loop counters, temporary expressions, and intermediate assignments disappear unless they can affect a later transition. Even initialization can sometimes be folded into the choice of an initial state. This is not code golf. A smaller state makes fewer distinctions between executions, so the essential behavior is easier to enumerate and the invariant is easier to see.

There is a hard constraint on that simplification: a state must contain everything needed to determine the permitted future. If two situations have identical abstract states but different legal next steps, some relevant information has been erased. A retry counter may be irrelevant in an unbounded mathematical protocol and essential in a service that stops after three attempts. A clock may be irrelevant to safety and essential to a lease. The right state is the smallest one that still explains every behavior the design promises to preserve.

Atomicity belongs to the model too. Combining several machine instructions into one abstract action asserts that observers cannot distinguish their internal order for the property being studied. Sometimes a lock, transaction, or single-threaded event loop justifies that assertion. Sometimes it conceals the race. Drawing action boundaries is therefore a design decision, not mere notation.

26:12–32:43 — Find the sentence that survives every step

With A as the original input, B as the unprocessed remainder, and X as the current candidate, the proof needs a bridge between progress and result. In the talk's formulation, the maximum represented by X together with the remaining values in B stays equal to the maximum of A. Processing one element changes the representation, but not that fact.[1][3]

That fact is an invariant. To use it, three obligations must remain distinct:

1. Show that every permitted initial state satisfies the invariant.
2. Assume the invariant before a permitted step and show it still holds afterward.
3. When the algorithm reaches its terminal condition, combine that condition with the invariant to obtain the promised result.

This is stronger than accumulating examples. A unit test might show that one ordering of [3, 1, 7] returns 7. The invariant explains why every permitted choice of the next element preserves the answer. It is also more diagnostic: if one transition does not preserve the statement, either the transition is wrong, the state is missing information, or the proposed invariant does not express the real reason the algorithm works.

The proof still does not establish termination. A system can preserve every safety invariant while taking steps forever. Lamport separates the question “can a bad state be reached?” from “must useful progress eventually occur?” For a service, progress may depend on scheduling fairness, eventual network delivery, timeouts, or bounded retries. Those are environmental assumptions and liveness obligations; leaving them implicit does not make them disappear.

33:15–38:58 — Refinement is where the model meets the repository

After the abstract algorithm is understood, implementation choices return. A mathematical extreme may become a language-specific minimum value, a tagged result, or an error. One abstract action may become several statements protected by a mutex. A bag may become an array with an index. These mappings are refinement decisions: the code is acceptable only if its observable behavior corresponds to an allowed abstract execution.

That is also the limit of model checking. TLC can explore the reachable states of a configured finite model and find a counterexample to a stated property. It does not prove that production code implements the model, that the model includes every hostile environmental behavior, or that the stated property is the one users actually need. A green model-checker run is evidence about a specification under assumptions, not a certificate for an unrelated binary.[4][5]

The payoff can still be substantial when the state space of the design is more dangerous than the size of the code suggests. An AWS engineering report describes using TLA+ specifications and model checking on difficult distributed-system designs, especially where conventional testing could not cover the vast combination of failures and concurrent events.[6] A later systematic review of a decade of industrial TLA+ practice found reported benefits alongside practical adoption challenges, a useful corrective to treating formal methods as either magic or ceremony.[7]

The keynote itself is deliberately broader than TLA+. Lamport says most everyday programs do not require a TLA+ specification. The transferable skill is to move between levels: write the behavioral idea clearly, choose state and steps when sequences matter, use an invariant when correctness spans those sequences, and reach for a formal language or model checker when the combinations outrun reliable informal reasoning.[1]

40:29–49:52 — Carry out a repeatable design ritual

The closing portion returns to writing. A precise explanation is not documentation applied after design; producing it is one of the ways design happens. If a maintainer cannot explain a retry loop without reciting its branches, the abstraction may still be missing. If an interface can only be described by pointing at an implementation, callers have no independent basis for deciding whether a surprising result is a bug.[1]

For a real OSS change, the talk's method can be reduced to a small ritual:

1. Write the result and failure behavior in terms visible to a caller, without naming the intended data structure or control flow.
2. List only the values that can affect future behavior. Challenge each one, and add back any fact whose removal would merge situations with different legal next steps.
3. Describe initialization and the allowed transitions, including failure, retry, cancellation, and recovery transitions.
4. Propose an invariant that connects the changing state to the promised result. Check initialization, preservation, and the terminal implication separately.
5. State progress assumptions explicitly. Decide what must eventually happen and which scheduler, clock, network, or operator behavior that depends on.
6. If interleavings or failures are combinatorial, encode a small finite model and ask a checker for counterexamples.
7. Map each important implementation path back to the model, then keep tests for the mapping, concrete edge cases, and integration behavior.

This does not require turning every pull request into a proof. A one-line formatter or a direct adapter may already be clearer as code. The ritual earns its cost when behavior depends on history: coordination, retries, caches, transactions, migrations, permissions, schedulers, or recovery after partial failure. In those areas, more code often makes the central argument harder to see.

Lamport's deceptively small maximum example supplies the lasting lesson. Correct programs do not emerge from syntax alone. They emerge when someone decides what the result means, chooses a state that preserves the relevant future, permits the right transitions, and discovers why no transition can break the promise. Code is where that argument runs. The design is the argument.

Sources

1. Southern California Linux Expo, “Coding Isn't Programming — Leslie Lamport,” SCaLE 22x closing keynote, YouTube video, March 9, 2025.
2. Southern California Linux Expo, “Closing Keynote with Leslie Lamport,” event page and program record, March 9, 2025.
3. Leslie Lamport, “Coding Isn't Programming,” official SCaLE 22x presentation slides.
4. TLA+ by Example, “Basic Operators” — the Init/Next pattern, actions, and primed variables.
5. TLA+ Foundation, tlaplus/tlaplus — source repository and documentation for the TLA+ command-line tools, TLC, PlusCal translator, and Toolbox.
6. Chris Newcombe et al., “How Amazon Web Services Uses Formal Methods,” Communications of the ACM, 2015.
7. Roman Bögli et al., “A Systematic Literature Review on a Decade of Industrial TLA+ Practice,” Integrated Formal Methods, 2025.
8. Wikimedia Commons, “File: Leslie Lamport September 2006.jpg” — photograph by Andrej Bauer, CC BY-SA 2.5 SI.