This video features an interview with Leslie Lamport, a Turing Award winner who made seminal contributions to distributed systems. Lamport shares fascinating stories about the background and development of his major works: the Bakery Algorithm, time and event ordering in distributed systems, the Byzantine Generals Problem, and the Paxos algorithm. He emphasizes that his ability to abstract was the key to his success, and makes a compelling case for the importance of writing and proof in clear thinking and problem-solving. He also shares personal experiences and philosophy — including why he chose industry over academia and his thoughts on a grand theory of large-scale concurrency — offering both practical and deeply considered advice to the next generation.

1. The Bakery Algorithm: Where Concurrent Programming Began 🍞

The interview opens with Leslie Lamport explaining his Bakery Algorithm. This algorithm was designed to solve the concurrent programming problem posed by Edsger Dijkstra in 1965 — specifically, the synchronization problem that arises when multiple processes simultaneously try to access a limited resource (such as a printer). Dijkstra framed this as the Critical Section concept: a region of code that only one process may execute at a time.

Lamport recounts how, in 1972, he came across an ACM paper on this problem and found it fascinating. He initially devised a simple algorithm for two processes, but quickly found a bug. This experience gave him a crucial insight: concurrent programs are very hard to get right, and you need a proof that they are correct. It left him with a stubborn determination — "damn it, I'm going to solve that problem."

"Concurrent programs were hard to get right and that you needed a proof that they were correct."

Lamport then drew inspiration from a deli counter — customers take a number and are served in order — and developed the Bakery Algorithm. Each process independently chooses a unique number, implementing the first-come, first-served principle without any central controller. What was particularly remarkable about this algorithm was that it works without assuming atomicity of shared registers. It was generally believed that problems arose when two processes read or wrote memory simultaneously, but the Bakery Algorithm was designed so that only one process writes to any memory location at a time, making it correct even in the presence of concurrent reads. This was considered impossible by the academic community at the time — even Lamport's colleague Anatol Holt initially didn't believe it. The Bakery Algorithm was significant because it was simpler than Dijkstra's existing solution and also satisfied the first-come, first-served property.

2. Working with Dijkstra: Discovering the Power of Abstraction ✨

Lamport shared his experience of working with Dijkstra and his colleagues in the Netherlands for a month in 1976. Dijkstra shared his ideas through short papers called EWDs (Edsger W. Dijkstra), one of which concerned the first Concurrent Garbage Collection algorithm — a method for automatically reclaiming memory no longer used by a program, which is especially complex in a concurrent environment.

When Lamport looked at Dijkstra's algorithm, he realized he could simplify the free list handling. Where Dijkstra maintained a separate process for the free list and had to coordinate it with other processes, Lamport integrated the free list as part of the ordinary data structure, eliminating any special handling. He thought the idea was trivially obvious, but Dijkstra was deeply impressed and included Lamport as a co-author. Lamport only later realized that the idea was far from obvious to most people, and that this had in fact been the moment his ability to abstract shone through.

"I later realized much later that it was not an obvious idea to most people and that that had actually impressed Dijkstra."

Dijkstra later told Lamport he had an "amazing ability to abstract", and after winning the Turing Award, Lamport came to understand that the secret to his success lay not in being especially smart, but in this capacity for abstraction. During his stay in the Netherlands, weekly discussions over beer with Dijkstra and Carl Holten led to a variant of the Bakery Algorithm that was eventually published as a paper.

3. His Most-Cited Paper: Time and Event Ordering in Distributed Systems ⏰

Lamport's most-cited paper is "Time, Clocks, and the Ordering of Events in a Distributed System." The idea arose while he was working on building a distributed database. People at the time were struggling to synchronize copies of data spread across multiple locations, and Lamport identified a fundamental problem: the actual order in which events occur can differ from the order in which the system perceives them.

Lamport drew inspiration from spacetime in special relativity. In special relativity, saying that one event happened before another means that a signal emitted by the first event was received before the second event occurred — and that signal cannot travel faster than light. Lamport applied this analogy to distributed systems and defined the "happens before" relationship: if one event can affect another by sending a message that carries information to it, then the first event happens before the second. This definition of "happens before" came as a major revelation to distributed systems researchers at the time.

Another important contribution of the paper was a method for building distributed systems using state machines. Lamport showed that a system can be modeled as a state machine — a sequence of states and commands — and that synchronizing these state machines can maintain consistency across a distributed system. He notes that while this seemed completely obvious to him, it was in fact a critically important concept for building distributed systems that many people overlooked.

"It it turned out that this was very obvious to me, but that's really in practice the important idea in that paper because it showed that this method of building distributed systems by thinking in terms of state machine and and can thinking about concurrent systems in terms of state machines."

Lamport emphasizes the importance of invariant proofs for understanding concurrent programs. Most approaches to reasoning about concurrent programs assume atomic operations and try to trace sequential execution, but this causes complexity to grow exponentially and is error-prone. By contrast, invariants — properties of system state that always hold true at each point in the program — allow correctness to be proved far more effectively. The complexity of invariant proofs scales quadratically with the number of processes, whereas reasoning via sequential execution scales exponentially.

4. The Byzantine Generals Problem: Reaching Consensus Among Traitors 🛡️

Lamport then tells the story of the Byzantine Generals Problem. Where the "Time, Clocks, and Ordering of Events" paper assumed a failure-free system, the Byzantine Generals Problem addresses distributed systems in which failures can occur. In particular, Byzantine faults represent the worst-case scenario, where processes do not merely crash but can exhibit arbitrary, malicious behavior.

Before joining SRI International, Lamport had been researching this problem and devised an algorithm using digital signatures — a technology that guarantees the authenticity of messages, under the assumption that a faulty process cannot forge another process's signature. Digital signatures were not yet widely known, but Lamport had been inspired by a conversation with his friend Whit Diffie and had developed one of the first digital signature algorithms (though impractical at the time, he proposed the idea of signing a hash of a document rather than the full document).

At SRI, he met colleagues who were working on a similar problem. They had developed a different algorithm that did not use digital signatures and required four processes to tolerate a single fault. Lamport's signature-based algorithm needed only three processes. The initial paper included both algorithms; the signature-free version was far more complex but contained a brilliant insight from Marshall Pease, Lamport recalls. Lamport later found a simpler inductive proof.

Lamport stressed that Byzantine faults are critically important in real-world settings like aircraft control systems, where computer failures can take arbitrary forms. During the 1970s oil crisis, pressure to develop fuel-efficient aircraft led to designs that were aerodynamically unstable and required computer control; because the nature of computer failures was unpredictable, solving the Byzantine fault problem was essential.

To spread awareness of this important result, Lamport realized — as Dijkstra had done with the Dining Philosophers — the value of wrapping a result in a compelling story. So he invented the name "Byzantine Generals Problem": a scenario in which four generals must jointly decide whether to attack, and one of them may be a traitor. He originally considered "Albanian Generals," but since Albanians are real people, he settled on the Byzantine Empire. The core of the problem was the fundamental question: how do you reach consensus in a distributed system that must tolerate arbitrary faults?

5. The Paxos Algorithm: A Practical Consensus Solution 🛠️

Lamport explains his other famous contribution: the Paxos Algorithm. Like the Byzantine Generals Problem, Paxos addresses the challenge of building a fault-tolerant state machine — making multiple computers cooperate to deliver a single, consistent service. But unlike Byzantine fault tolerance, Paxos assumes only the far more common "crash" faults seen in industry, where a process simply stops or halts.

Lamport devised Paxos in 1985 after joining DEC SRC (Digital Equipment Corporation Systems Research Center), where he was working on a distributed operating system. The DEC SRC team were alumni of Xerox PARC — the inventors of Ethernet and the pioneers of distributed personal computing. They had system code that kept shared storage consistent, but Lamport felt it was "code, not an algorithm." Here he articulates his philosophy: an algorithm is more abstract than a program, and when building concurrent systems, the synchronization problem should be solved at the abstract algorithm level rather than wrestling with code-level complexity.

"An algorithm is something that's more abstract than a pro than than a program... It's something that's that's at a higher level of of of abstraction."

After it was developed, Paxos sat unpublished for eight years before appearing under the title "The Part-Time Parliament." Early reviewers had not recognized its importance. But colleagues like Butler Lampson grasped the value of the Paxos idea and began using it to build systems, spreading the idea organically, and Lamport was in no hurry to publish. Eventually a new editor helped revise and expand the paper into publishable form.

Lamport wove an amusing backstory around the Paxos paper, framing it as a document discovered on the ancient island of Paxos. He even appeared at his talk dressed as an Indiana Jones–style archaeologist. Yet he recalls that the audience at the time did not truly grasp the algorithm's significance — only Butler Lampson did, because of his deep understanding of what it takes to build distributed systems.

6. Paxos vs Raft ⚖️

Lamport shares his views on the Raft Algorithm, which solves a similar problem to Paxos. When Raft's authors sent him a draft, he replied: "Bring me an algorithm or bring me a proof." Lamport believes Raft is fundamentally the same idea as Paxos, described differently.

Paxos is divided into two phases: leader election (phase 1) and decision-making (phase 2). As long as the leader does not change, phase 1 needs to be executed only once. Raft, Lamport argues, describes these in reverse order — it continues phase 2 until the leader fails, then falls back to phase 1. He says he cannot understand why Paxos is considered hard to understand, and claims he can explain it in five minutes.

Raft's developers argued it was simpler and easier to understand, and experiments with students seemed to confirm this. But Lamport recounts an important anecdote:

"There was a bug discovered in Raft and fixed, but I believe that the algorithm that they found more understandable was one with that bug."

This made him reconsider what "understanding" really means. To Lamport, genuine understanding means "being able to write a proof"; but for most people, understanding is closer to a "warm fuzzy feeling." Raft's presentation gave programmers that warm feeling — but the fact that it contained a bug shows that intuitive understanding does not guarantee correctness. Lamport believes his way of explaining Paxos provides deeper insight into why the algorithm actually works.

7. Developing LaTeX: Why Writing Improves Thinking ✍️

Lamport also tells the story of his other major contribution: developing LaTeX. When he began writing a book, he needed to use the TeX typesetting system, but found he needed macros to do what he wanted. He decided to put in a little extra effort and make those macros available for others to use.

LaTeX follows the approach of describing a document's logical structure and letting the system handle formatting automatically — an idea he borrowed from the earlier Scribe system. Lamport held the abstractionist view that ideas matter, not typesetting. He collaborated with publishers' editors to develop LaTeX's standard styles. All of this work, he confesses with a laugh, was done in his "spare time" — officially, his hours were allocated to other projects.

He returns to his well-known maxim about why writing improves thinking:

"If you're thinking without writing, you only think you're thinking." "If you think you know something but don't write it down, you only think you know it."

This is especially important for people building computer systems. If you think an idea will work, or that others will use it, write it down and explain it. He cites the old adage — "write the manual before you write the program" — and notes that while writing the LaTeX book, wherever something was hard to explain, he realized the algorithm itself needed to change.

Writing promotes clear thinking precisely because it is so easy to deceive yourself. Lamport connects this to his philosophy of writing proofs. As he worked on proofs for complex concurrent algorithms, he realized there were too many details for traditional mathematical proof style to handle. So he devised a hierarchical proof structure: break the whole problem into smaller steps and provide a proof for each step. This ensures every detail of the proof is made explicit and nothing is omitted.

When Lamport introduced this hierarchical proof style to mathematicians, he was met with furious opposition. He believes their irrational reaction stemmed from a fear that they would be forced to write proofs that a computer could check.

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

He explained that his approach required no greater formality — it was simply a matter of organization — but the mathematicians pushed back, insisting they had no desire to "write proofs for computers." Lamport argues that the reason his method demands more work is precisely because it surfaces what was previously hidden: it forces you to make explicit the steps you took for granted, reducing errors and forcing genuine intellectual honesty.

8. Why Industry Instead of Academia, and a Grand Theory of Concurrency 💡

Lamport spent his entire career doing research in industry. He admits he did not even realize he was "doing computer science" until the mid-1970s, when he came to understand it was an academic discipline. He simply never felt that computer science needed to be taught at a university, and wasn't sure teaching would be enjoyable.

Lamport addresses a question about a footnote in which he once felt he had failed to develop a grand theory of concurrency. Many researchers sought an abstraction that could capture the essence of concurrent computing the way the Turing machine captured the essence of sequential computing. Attempts like Petri nets were made, but Lamport notes that most were language-based. He was always more interested in what a language expresses — the ideas — than in the language itself.

He now believes the Turing machine equivalent for concurrent computing is the State Machine — defined, in his formulation, even more simply: no commands, just states and a relation between states and their successors. However, this state machine does not provide the same power as a Turing machine. Where the Turing machine describes what is computable, the state machine describes anything — any behavior can be described by one. For example, when you say a variable can hold "any integer," constraining it to finite computer integers only makes things more complicated. Infinity was introduced to simplify things, not complicate them.

"The people have this funny idea that you know because something is infinite it's more complicated. They got it backwards. Infinity was introduced to simplify things."

Lamport criticizes the tendency of computer scientists and programmers to fixate on languages. They invent all manner of languages and believe those languages improve their thinking. But Lamport argues that mathematics is the most powerful tool for understanding, and that attempts to handle concurrency in ways that resemble programming languages are fundamentally misguided. Programming languages exist for efficiency, but when it comes to understanding, nothing beats mathematics.

9. "I Don't Think I'm That Smart" — Advice for the Next Generation 🧠

Despite his accomplishments, Lamport has often said he does not consider himself especially smart. He explains that he frequently found things others struggled with to be easy or straightforward, but because it all felt natural to him, he never recognized his own distinctiveness.

He alludes to a phenomenon psychologists describe: people who are highly skilled at something often don't realize how good they are, precisely because it feels easy to them. Conversely, people who are bad at something tend to overestimate their own ability. Lamport puts it more bluntly:

"Stupid people think they're smart because they're too stupid to realize they're not."

His gift lies in abstraction, and it has only been in the past decade or so that he has come to appreciate just how much better at it he is than most people.

Finally, asked what advice he would give his younger self, Lamport says the lesson he learned early in life is this:

"One thing I've learned fairly early in my life is that I shouldn't waste time trying to answer questions that I don't have to answer."

He says he doesn't dwell on questions like "what should I have done differently" — because those are questions he doesn't need to answer. This reflects his practical, present-focused attitude: concentrate on what's in front of you and don't burn energy on needless rumination.

Closing Thoughts

The conversation with Leslie Lamport was a session of deep insight — not only into distributed systems, but into the importance of clear thinking, abstraction, and the role of proof through writing. His experience shows that solving technical problems is about far more than writing code; it is about the underlying ideas and the process of proving those ideas correct. His message — "if you're thinking without writing, you only think you're thinking" — resonates for every engineer and researcher. When building complex systems, do not rely on intuition alone. Clear algorithms and rigorous proof are how you reduce errors and build something you can truly trust.