This interview with Turing Award winner Leslie Lamport covers the backgrounds and development of his major work: the Bakery Algorithm, distributed systems time and event ordering, the Byzantine Generals Problem, and the Paxos algorithm. He emphasizes that his ability to abstract was the key to his success, and passionately advocates for the importance of writing and proofs for clear thinking and problem-solving.

1. The Bakery Algorithm: Beginnings of Concurrent Programming

Lamport developed the Bakery Algorithm inspired by deli counters where customers take numbered tickets. It solved Dijkstra's 1965 mutual exclusion problem while being the first to implement first-come, first-served ordering. Remarkably, it worked without assuming atomic shared memory operations -- a feat his colleague Anatol Hol initially didn't believe was possible. His early bug in a 2-process solution taught him that concurrent programs are hard to get right and need correctness proofs.

2. Working with Dijkstra: Discovering Abstraction

During a month with Dijkstra in the Netherlands in 1976, Lamport simplified a concurrent garbage collection algorithm by integrating the free list into the general data structure -- eliminating the need for a separate coordination process. Dijkstra was deeply impressed. Lamport later realized this was his abstraction ability at work. After winning the Turing Award, he understood that his success came not from being particularly smart but from this "amazing ability to abstract."

3. The Most-Cited Paper: Time, Clocks, and Event Ordering

Lamport's most-cited paper arose from building a distributed database. Inspired by special relativity's spacetime concept, he defined the "happens before" relation for distributed systems -- one event precedes another only if information could have traveled between them via messages. This definition shocked the distributed systems community. The paper also introduced the idea of building distributed systems as state machines -- obvious to Lamport but immensely important in practice.

He stresses the importance of invariant proofs for concurrent programs. Invariant proof complexity grows quadratically with process count, while sequential reasoning grows exponentially.

4. The Byzantine Generals Problem

The Byzantine Generals Problem addresses arbitrary malicious failures in distributed systems. Lamport developed algorithms using digital signatures (needing only 3 processes for one fault) and without signatures (needing 4 processes). He named it the "Byzantine Generals Problem" to make it memorable -- like Dijkstra's "Dining Philosophers" -- originally considering "Albanian Generals" but switching because Albanians are real people.

5. The Paxos Algorithm

Paxos solves fault-tolerant state machine construction for crash failures (simpler than Byzantine faults). Developed at DEC SRC in 1985, the algorithm took 8 years to publish because initial reviewers didn't recognize its importance. Only Butler Lamson saw its true value. Lamport wrapped the paper in a fictional story about documents found on the ancient island of Paxos and once presented dressed as an Indiana Jones-style archaeologist.

6. Paxos vs Raft

Lamport considers Raft essentially the same idea as Paxos, explained differently. Paxos has two phases: leader election (phase 1) and decision-making (phase 2). Raft runs phase 2 until the leader fails, then returns to phase 1 -- the reverse order. Lamport says he can explain Paxos in 5 minutes and doesn't understand why people find it hard. Notably, a bug was discovered in Raft -- and Lamport believes the version people found "more understandable" was the one with the bug.