In this episode of First Principles by a16z Crypto, host Tim Roughgarden (Head of Research) and co-host Itay Abraham (Research Partner) sit down with Turing Award-winning computer scientist Dr. Leslie Lamport. The conversation spans the history of distributed systems, beginning with Lamport's early work on concurrency, the bakery algorithm, and logical clocks. Lamport explains how he developed the state machine replication model and the Byzantine Generals Problem to address fault tolerance in complex systems. He details the origins of the Paxos consensus protocol, which sacrifices theoretical liveness to guarantee safety in asynchronous networks.

The hosts discuss Donald Knuth's famous assertion on programming aptitude, often associated with The Art of Computer Programming, and how Lamport's upcoming book, A Science of Concurrent Programs, aims to teach rigorous mathematical abstraction. Finally, Lamport shares how working in industrial research labs provided real-world inspiration, drawing a parallel to the artistic philosophy found in Jean Renoir's autobiography, My Life and My Films, before the hosts reflect on how government-funded survivability research ultimately shaped modern blockchain infrastructure.

The Genesis of Concurrency and the Bakery Algorithm

Leslie Lamport entered the field of concurrency in 1972 after reading a mutual exclusion algorithm in the Communications of the ACM (CACM).

After his initial attempt at a simple two-process solution was rejected due to a bug, Lamport realized "how tricky concurrency is, and how you really have to be able to prove the correctness of a concurrent algorithm." - Leslie

This realization led directly to the creation of the bakery algorithm, which served as the foundation for all of Lamport's work over the subsequent three years.

By 1978, while writing a correctness proof for a government contract at SRI, Lamport discovered "there's no basic difference in how you reason about non-distributed or distributed concurrent algorithms." - Leslie

State Machine Replication and Byzantine Faults

Lamport introduced the state machine abstraction to ensure multiple processes execute the same commands in the same order, a concept central to modern blockchains.

"The general problem is really getting multiple processes to all be doing the same thing." - Leslie

To address hardware failures, Lamport formulated the Byzantine Generals Problem, assuming the most general fault model where a "failed process could do anything." - Leslie

Lamport notes that while he initially assumed digital signatures could easily solve Byzantine faults, early aerospace engineers at SRI avoided them, requiring 3n + 1 computers instead of 2n + 1 to tolerate n faults.

The Paxos Protocol and the Story of the Parliament

The Paxos protocol emerged when Lamport attempted to write an impossibility proof for a crash-tolerant local area network system.

"The problem that Paxos has is in principle, basically it's implementing a state machine, but that with failures it could take forever for the computers to come to a decision." - Leslie

Paxos bypasses the impossibility result of Fischer, Lynch, and Paterson by giving up theoretical liveness while strictly maintaining safety.

Lamport admits that framing the Paxos paper around a fictional Greek legislative system "was a flop" that "confused people and put them off" rather than making it accessible.

Bridging Academic Theory and Industrial Reality

Lamport attributes his success to thinking of concurrency as a physical problem of "real computers, real electrons flowing" rather than a language or mathematical construct.

Working in industrial research labs provided Lamport with a vast array of real-world problems that academic settings lacked.

To explain his preference for industry, Lamport references Jean Renoir's autobiography My Life and My Films, where Renoir's father noted that painting outdoors reveals "thousands of different kinds of leaves" compared to the few one can imagine in a studio.

Tim Roughgarden and Itay Abraham discuss Donald Knuth's famous quote, often associated with his monumental work The Art of Computer Programming, that only 2% of the population is naturally suited to be programmers.

Formalizing Correctness with TLA+ and Modern Theory

To help system designers think more abstractly, Lamport developed TLA+ (Temporal Logic of Actions), a formal specification language.

Lamport's upcoming book, A Science of Concurrent Programs, consolidates his lifetime of research on the underlying mathematical theory of concurrent algorithms.

The primary objective of A Science of Concurrent Programs is to teach designers how to "state very precisely what the problem is... and show mathematically and with tools that this algorithm satisfies the correctness property." - Leslie

The book is scheduled for publication by Cambridge University Press in March 2025.

The Long-Term Evolution of Survivability Systems

Itay Abraham points out that Byzantine agreement was originally funded by DARPA to ensure the "survivability of systems" against physical or malicious attacks.

The technology has transitioned from government-focused defense use cases to driving economic value in modern public blockchains like Ethereum and Solana.

Tim Roughgarden highlights that blockchain technology is now "reaching a maturity state where it's giving gifts back" by pushing the state of the art in cryptography and SNARK design.