图灵奖得主 Leslie Lamport：清晰思考、Paxos 与 Raft，以及与 Dijkstra 共事 | Ryan Peterman
这场对谈沿着 Leslie Lamport 五十余年的工作脉络，串起面包店算法、与 Dijkstra 的交往、happens-before、状态机与不变量、拜占庭将军问题、Paxos、Raft、LaTeX，以及他对写作、证明和抽象的长期看法。Lamport 反复强调：并发系统真正困难的不是把代码写出来，而是找到合适的抽象、明确系统状态，并写下能够经受检查的证明。他也解释了为何自己更看重“能证明”的理解，而不是一种直觉上舒服的感觉；以及为什么数学、状态机和写作会迫使人暴露尚未说清楚的部分。