Turing Award Winner: Thinking Clearly, Paxos vs Raft, Working With Dijkstra | Leslie Lamport

ELI5/TLDR

Leslie Lamport is the person behind most of the foundational ideas in distributed computing — how multiple computers work together without stepping on each other’s toes. His secret weapon was not raw intelligence but an unusual talent for abstraction: stripping problems down to their essential structure. He believes most programmers skip the hard part (thinking clearly and writing things down) and jump straight to code, which is why concurrent systems are so full of bugs. His advice boils down to: if you haven’t written it down, you don’t actually understand it.

The Full Story

The Bakery Algorithm: A Deli Ticket for Computers

Lamport’s origin story in concurrency begins with hubris. In 1972, he saw a published solution to Dijkstra’s mutual exclusion problem — how to ensure only one process uses a shared resource at a time, like a printer — and thought it looked needlessly complicated. He dashed off a simpler version and submitted it. A couple weeks later, the editor wrote back pointing out the bug.

Two things came out of that humbling experience. First, that concurrent programs are genuinely hard to get right, and you need a mathematical proof they work. Second, a stubborn determination to actually solve the problem.

The result was the bakery algorithm. The idea is borrowed from a deli counter: each process takes a numbered ticket, and the lowest number gets served first. The twist is there’s no central ticket dispenser — each process picks its own number. What made the proof remarkable was a property everyone thought was impossible: the algorithm still worked even if one process read garbage data while another was writing. No atomic operations required.

“I wrote the proof on the whiteboard for him and he couldn’t find anything wrong with it, but he went home saying there must be something wrong with it.”

His colleague Anatol Holt simply refused to believe the result. He never did find the flaw, because there wasn’t one.

Time, Clocks, and Stealing From Einstein

Lamport’s most-cited paper came from noticing that a distributed database solution had a subtle problem: it guaranteed operations would appear sequential, but the sequence might not match the order they actually happened in. Most people wouldn’t see that as a problem. Lamport did, because he’d studied special relativity.

In physics, event A “happens before” event B only if a signal from A could reach B — limited by the speed of light. Lamport realized distributed systems have the same structure, except the speed limit is message-passing between computers instead of photons. He mapped the physics concept directly onto computer science.

“The notion of happens before is exactly the same as in relativity except instead of being whether one event can influence another by things traveling at the speed of light, it’s whether the first event could have affected the other by information sent over messages.”

The paper also introduced the idea of describing distributed systems as state machines — which Lamport considers the actually important contribution. People ignored that part entirely. Twice, colleagues told him the paper contained nothing about state machines. He had to go reread his own paper to confirm he wasn’t losing his mind.

Why Invariants Beat Sequence Reasoning

Lamport makes a case for understanding programs through invariants — properties of the system’s state that remain true at every step — rather than tracing through sequences of events. The number of possible execution sequences grows exponentially with the number of processes. The complexity of an invariant proof grows quadratically. That’s not a minor difference. That’s the difference between “tractable” and “good luck.”

Byzantine Generals: Marketing Matters

The Byzantine fault tolerance work started at SRI, where engineers were building computers to fly airplanes. The 1970s oil crisis pushed aircraft manufacturers toward smaller control surfaces for fuel efficiency, which made planes aerodynamically unstable. Humans couldn’t compensate fast enough; computers could. But how many backup computers do you need?

Everyone assumed three computers could tolerate one failure. Lamport and colleagues proved you actually need four (or three, if you use digital signatures). The key insight: a “Byzantine” fault means a component can do anything — send contradictory messages, lie, act maliciously. Under those conditions, three-out-of-three voting doesn’t work.

Lamport had learned from Dijkstra that a good story sells a result. Dijkstra’s dining philosophers problem wasn’t particularly deep, but the image of philosophers fighting over forks made it unforgettable. So Lamport invented Byzantine generals besieging a city, some of whom might be traitors. He initially wanted “Albanian generals” — Albania being a Cold War black hole — but his boss pointed out that Albanians exist. Byzantines, on the other hand, are safely extinct.

“I realized that Byzantine — there aren’t any Byzantines around and that was the perfect name.”

A Boeing engineer, on reading the paper, had a beautifully pragmatic reaction: “Oh, we need four computers.”

Paxos: The Paper Nobody Understood

Paxos solves the same fundamental problem as the Byzantine generals work — building a fault-tolerant state machine — but for the more common case where failures mean a computer simply stops rather than going rogue. Lamport discovered it almost by accident, while trying to prove that what his colleagues at DEC SRC were doing was impossible. Partway through the impossibility proof, he realized he was actually writing an algorithm.

He presented the paper dressed as an Indiana Jones-style archaeologist, because the paper was framed as a fictional account of an ancient Greek parliament on the island of Paxos. Nobody understood it. The paper sat for eight years before being published. Butler Lampson was the rare person who grasped both the algorithm and its implications, and he championed it.

“I think the lecture may have gone well, but I think nobody understood the algorithm or nobody understood the significance of the algorithm.”

Paxos vs. Raft: Understanding vs. Warm Fuzziness

When the Raft authors sent Lamport their draft, he sent it back with something like “come back when you have a proof.” His assessment: Raft is essentially Paxos explained in reverse order (steady-state first, leader election second) with some practical details filled in. It’s the order engineers prefer to think about things, which is why they find it more intuitive.

But there’s a punchline. A bug was discovered in Raft and later fixed. Lamport believes the version students rated as “more understandable” was the one with the bug.

“What understanding means for most people is a warm fuzzy feeling.”

For Lamport, understanding means you can write a proof. For most people, it means the explanation feels right. These are not the same thing, and the gap between them is where bugs live.

LaTeX: A Side Project on Company Time

LaTeX started because Lamport needed macros for a book he was writing using TeX. He figured a little extra effort could make them usable by others. The design philosophy came from an earlier system called Scribe: describe the logical structure of a document, and let the system handle formatting. He built it in six to nine months of what he delicately describes as time billed to projects that had nothing to do with it.

Writing as Thinking

Lamport’s most quotable line: “If you think you know something but don’t write it down, you only think you know it.”

He arrived at this through writing proofs of concurrent algorithms. With a PhD in math, he knew how to write proofs — but the standard approach fell apart when concurrency multiplied the details beyond what he could track. His solution was hierarchical structured proofs: each step cites exactly which prior steps it depends on. No hand-waving. No “it’s obvious.”

When he tried showing this to mathematicians, about twenty of them, they got angry. He thought they might physically attack him. His theory: the anger comes from fear — fear of being forced to make their reasoning explicit, which would reveal the gaps.

“Their reaction shocked me. They became angry. I really thought they might physically attack me.”

Abstraction as Superpower

Lamport spent decades not realizing what made him effective. He didn’t think of himself as particularly smart. Only after winning the Turing Award did he identify the pattern: his gift was abstraction. Dijkstra spotted it decades earlier, when Lamport sent him a simplification to a garbage collection algorithm that seemed obvious to Lamport but was not obvious to anyone else.

“Stupid people think they’re smart because they’re too stupid to realize they’re not.”

His version of the Dunning-Kruger effect, stated with characteristic economy. The flip side: people who are genuinely good at something don’t notice, because it’s easy for them.

The Turing Machine of Concurrency

Lamport once felt like a failure because he wanted to find the grand unifying theory of concurrency — the equivalent of what Turing machines are for sequential computation. He now believes state machines are that thing, just without the neat boundary of “what’s computable” that Turing machines provide. State machines can describe anything, including impossible things, which is actually a feature: real-valued integers simplify reasoning the same way infinite number lines simplify arithmetic.

“People have this funny idea that because something is infinite it’s more complicated. They got it backwards. Infinity was introduced to simplify things.”

Asked what advice he’d give his younger self, he declined on principle.

“I shouldn’t waste time trying to answer questions that I don’t have to answer.”

Claude’s Take

This is a genuinely excellent interview with someone who has earned every word of deference he receives. Lamport’s contributions to distributed systems are not debatable — they’re the load-bearing walls of modern computing infrastructure. What makes this conversation particularly valuable is not the technical content (which is well-documented elsewhere) but the metacognitive thread running through it: how does clear thinking actually work?

His central thesis — that writing forces honest thinking, that abstraction is more valuable than raw intelligence, that “understanding” without proof is just comfort — is both well-supported by his track record and somewhat undercut by his own blind spots. He dismisses programming languages as distractions from mathematical reasoning, which is true at the algorithm design level but ignores the reality that most software engineering is not algorithm design. The vast majority of bugs in production systems are not concurrency errors in consensus protocols; they’re off-by-one errors in business logic and misconfigured YAML files.

His take on Raft is entertaining but slightly ungenerous. Yes, Raft had a bug. So did Lamport’s first attempt at the mutual exclusion problem. The Raft authors’ contribution was making consensus accessible to working engineers, which has real value even if it doesn’t satisfy Lamport’s definition of “understanding.” There’s a reason Raft is used in more production systems than Paxos: people can implement what they can understand, warm fuzziness and all.

The mathematicians-nearly-attacking-him anecdote is striking. His interpretation (fear of exposure) is plausible but incomplete. Mathematicians have centuries of developed intuition about which gaps in proofs are genuine problems and which are rhetorical shortcuts between consenting adults. Lamport’s structured proofs solve a real problem in concurrent systems verification, but presenting them as universally superior to traditional mathematical proof-writing is the kind of overreach that gets people’s hackles up.

Still, his core message lands. Most people writing concurrent code have no algorithm, no proof, and no invariant. They have code and hope. Lamport has spent fifty years saying this, and fifty years of distributed systems failures keep proving him right.