To ensure his critical work on fault tolerance was widely understood, Lamport created the "Byzantine Generals" narrative. He learned from Dijkstra's "Dining Philosophers" that a memorable story is key to an idea's popularity and adoption, even if the underlying problem is complex and highly technical.
When Leslie Lamport suggested mathematicians adopt a hierarchical structure for proofs, the reaction was not academic debate but pure anger. He speculates the hostility stemmed from a fear that such rigor would expose unstated assumptions and force them to write proofs detailed enough for a computer to verify, revealing flaws in their thinking.
Lamport's Bakery Algorithm solved a major concurrency problem. Its most surprising feature was its ability to function correctly even if a process reads a garbage value while another is writing. This property was so counter-intuitive that his colleagues initially refused to believe the proof was correct.
Lamport emphasizes the critical distinction between an algorithm and code. An algorithm is the abstract, high-level solution, while code is just one implementation. He argues that engineers often mistakenly jump directly to code, conflating core synchronization problems with irrelevant implementation details, which leads to flawed systems.
Lamport argues that writing is a critical tool for clear thinking. It forces you to confront fuzzy ideas and hidden assumptions, preventing self-deception. This principle applies to writing proofs, system specifications, or even user manuals before coding. The act of writing reveals flaws and makes you honest.
Leslie Lamport challenges the notion that Raft is superior to Paxos because it's more "understandable." He points out that a bug was found in the very version of Raft that students preferred, suggesting their understanding was superficial. For Lamport, true understanding means being able to write a proof, not just having a "warm, fuzzy feeling."
Lamport offers a blunt assessment of intelligence, echoing the Dunning-Kruger effect. He attributes his own success not to "raw intelligence" but to a specific gift for abstraction that comes easily to him. This contrasts sharply with those who overestimate their abilities because they lack the competence to recognize their own shortcomings.
Leslie Lamport reveals that the concept of using state machines to build distributed systems was a key part of his seminal "Time, Clocks" paper. However, this practical idea was completely overshadowed by the more theoretical "happened-before" relation. He had to reread his own paper to confirm he wasn't "going crazy" when people claimed it wasn't there.
