The Peterman Pod Turing Award Winner On Thinking Clearly, Paxos vs Raft, Working With Dijkstra | Leslie Lamport
63 snips
Feb 23, 2026 Leslie Lamport, Turing Award–winning computer scientist behind Paxos and Lamport timestamps. He tells stories about the Bakery algorithm, working with Dijkstra, the happens-before concept, inventing Byzantine faults, and the Paxos vs Raft debate. He also shares why writing and state-machine thinking shaped his work and how practical problems guided his research.
AI Snips
Chapters
Transcript
Episode notes
Working With Dijkstra In The Netherlands
- Lamport spent a month in the Netherlands working with Edsger Dijkstra and collaborators, contributing a simplification to concurrent garbage collection.
- Dijkstra later made Lamport a co-author and noted Lamport's gift for abstraction, which impressed him.
Happens Before And State Machine Thinking
- The 'happens-before' relation maps distributed events to causality like special relativity, enabling partial ordering of events via message transmission.
- This led Lamport to advocate state machines and invariants as superior methods for reasoning about concurrency compared to enumerating execution sequences.
Prove Concurrency With Invariants Not Execution Sequences
- Use invariants to understand and prove concurrent programs instead of reasoning about all possible execution sequences.
- Invariance proofs scale much better: they avoid exponential sequence complexity and reduce reasoning to manageable pairwise relationships.