【摘要】数学家出身的 Leslie Lamport 也是杰出的计算机科学家，LaTex、逻辑时钟，以及对分布式系统至关重要的 Paxos 共识算法都是他的手笔。Lamport 强调规范语言对于复杂系统开发的重要性，并为之开发了 TLA+。由于在分布式系统领域作出的突出贡献，Lamport 获得了图灵奖。

【标签】#计算机历史 #人物 #分布式计算 #Paxos #LaTeX #TVL+

【题图】Talia Herman for Quanta Magazine

作者：Sheon Han｜译者：常真｜校对：Roy｜排版：Queeny

Leslie Lamport 彻底改变了计算机之间的对话方式。现在他正在研究工程师如何与他们的机器对话。

由于计算机科学家 Leslie Lamport 的工作，现代计算机可以有效地相互协同。此后，他将注意力转向了如何让编程本身更有效率。

Leslie Lamport 也许不是一个家喻户晓的名字，但计算机科学家知道，排版系统 LaTeX 和让谷歌和亚马逊云基础设施得以实现的技术的背后都有他的身影。他还给几个问题起了独特的名字，让人们更加关注，如面包房算法和拜占庭将军问题。这绝非偶然。这位 81 岁的计算机科学家，对人们如何使用和思考软件有着不同寻常的想法。

2013 年，他获得了图灵奖（计算机领域的诺贝尔奖），表彰他在分布式系统方面的工作。分布式系统让不同网络上的多个组件相互协同来实现共同目标。互联网搜索、云计算和人工智能都涉及协同很多强大的计算机器一起工作。当然，这种协同会让你遇到更多的问题。

Lamport 曾经说过：“在分布式系统中，一台你甚至都不知道的计算机发生了故障，就能让你自己的计算机无法使用。”

最大的麻烦中有一个是 ＂并发系统＂，即在相互重叠的时间片段内发生多个计算操作，导致了二义性。哪台计算机的时钟是正确的？在 1978 年的一篇开创性的论文中，Lamport 借用狭义相对论的见解，引入了＂因果关系＂的概念来解决这个问题。两个观察者可能对事件的顺序有异议，但如果一个事件导致了另一个事件的发生，就消除了二义性。发送或接收一条信息可以在多处理中建立因果关系。逻辑时钟——现在也被称为 Lamport 时钟——提供了一种并发系统推算的标准方法。

有了这个工具，计算机科学家接下来想知道，他们如何能够系统性地扩大相互连接的计算机，而不增加错误。Lamport 想出了一个优雅的解决方案：Paxos，一种允许多台计算机执行复杂任务的 "共识算法"。没有 Paxos 和它的系列算法，现代计算机系统就不可能存在。

20 世纪 80 年代初，在拓展该领域的同时，Lamport 还创建了 LaTeX。这是一个文件预处理系统，为复杂公式的排版和格式化科学文献提供了精巧的方法。不仅在数学和计算机科学领域，LaTeX 在大多数科研领域都已成为论文的格式标准。

自 20 世纪 90 年代以来，Lamport 将工作重点转向了＂形式验证＂，即使用数学证明来验证软件和硬件系统的正确性。值得注意的是，他创造了一种名为 TLA+（Temporal Logic of Actions，行为时序逻辑）的 "规范语言"。软件规范就像程序的蓝图或食谱；它描述了软件在高层次上应该如何表现。这并不总是必要的，因为编写简单的程序就跟煮鸡蛋差不多。但是，更加复杂的高风险任务对精确度的要求也更高——此时的编码工作相当于烹制满汉全席。你需要为每道菜备好食材，精心配制，再分毫不差地端上桌给供位客人享用。这就要用到以简练明晰的语言写成的正确食谱和烹饪说明了，而用英语随意写出来的描述就可能会造成误解。TLA+ 采用精确的数学语言来防止错误，避免设计缺陷。

使用食谱或规范作为输入，一个被称为模型检测器的程序将检查食谱是否合理，是否能够按照预期来工作，按照厨师的要求制作出菜肴。Lamport 感叹程序员经常在写出适当规范之前就拼凑出一个系统，然而，厨师们在不知道食谱是否有效的情况下，可不会答应承办宴会的。

Quanta（译注：发表本文的杂志）与 Lamport 谈了他在分布式系统方面的工作，计算机科学教育出现的问题，以及如何使用 TLA+ 帮助程序员开发更好的系统。为使文意清晰，采访内容经过了精简和编辑。

让我们先聊聊 Paxos 这个非常有影响力的算法。起初是什么让你开始研究它的？

那时人们正在用一些代码来开发系统，而我有一种预感，他们的代码不可能实现预期目标。因此，我决定尝试证明这一点，结果想出了一个算法。这个算法本来就应该在人们的系统中使用。

他们的原始算法有什么问题？

嗯，他们没有算法，只有一堆代码。很少有程序员用算法来思考问题。当你试图编写一个并发系统时，如果在没有算法的情况下写代码，你的程序就不可能没有一堆错误。

介绍 Paxos 的论文起初并没有广泛传播，为什么？

人们阅读那篇论文有困难的原因是，我喜欢用故事来解释事情，而且会用某种伪希腊字母为故事里的人物起名字。比如这篇论文中，有一个名叫 Γωυδα 的奶酪质检员。作为一名数学家，我天天跟希腊字母打交道，只是不知道别人会被这些字母吓坏。很明显，读者不吃这一套，于是那篇论文没有得到应有的阅读量。

所以一开始它的阅读量不佳。虽然长期来看它得到了应有的重视，但那也是因为人们给这套共识算法起了个好名字：Paxos，而不是＂Viewstamped Replication＂，后者是计算机科学家 Barbara Liskov 同一算法的另一个名称。

在分布式系统方面工作了这么多年，是什么让您转而开发 TLA+ ？

在 20 世纪 70 年代，人们对程序进行探究，试图用编程语言来证明程序自身的属性。后来，人们意识到应该首先说明程序应该完成什么——也就是程序的行为。

20 世纪 80 年代初，我意识到，为并发系统编写这些更高级规范的实用方法，是把它们写成抽象的算法。有了 TLA+，我就能以一种非常严谨的数学方式来表达它们，然后就一切都合拍了。这里讲的是，不要试图用编程语言来写算法。如果真的想把事情做好，你需要用数学语言来写算法。

你说过，"如果只思考不撰写文档，那你只是自以为是"。这就是模型检测的作用吗？

模型检测是一种测试方法，它会对系统模型的所有执行进行穷尽测试。它只说明模型的正确性，而不是算法的正确性。当模型检测对正确性进行测试时，编码只是生成代码，它并不测试任何东西。在模型检测出现之前，确保算法有效的唯一方法是写出证明。

在实践中，模型检测会检查算法实例的所有执行情况。如果你很幸运，可以检查足够多的实例，让你对该算法更有把握。但是，对于任何规模的系统和算法的任何运用，这个证明都可以验证其正确性。

听起来，模型检测与另一种程序验证方法有关：使用 Coq 等工具进行交互式定理证明。它们有什么不同？

Coq 是专为解决数学问题设计的，并且能够采集记录数学家所做的推理。例如，Georges Gonthier 就是用它来证明四色定理的。一个数学命题的证明经过机器验证后，几乎可以肯定该命题为真。

TLA+ 不是为数学家设计的，而是为那些想证明系统属性的工程师设计的。20 世纪 90 年代，在花了大约 15 年时间编写并发算法的证明之后，我学会了为证明并发算法的正确性需要做什么。TLA 是一种逻辑，它能让所有的证明过程具有完备的形式化逻辑。而 TLA+ 则是基于此的一套完整语言。

像 TLA+ 这样的规范语言在业界的应用并不广泛，对吗？你认为这是为什么呢？

好吧，我正在尽自己的一份力。但基本上程序员和许多（如果不是大多数）计算机科学家都被数学吓坏了。所以它很难推广。

第二，每个项目都要匆匆完成。有一句老话，"永远没有时间把事儿做对，但总有时间重新来过。"因为 TLA+ 涉及前期工作，相当于在开发过程中增加了一个新的步骤，这也让它的采用变得困难。

前期的工作是否总是值得？

诚然，世界各地的程序员所写的大部分代码，确实不需要非常精确的文档来说明它应该如何运行。但是，有些非常重要的事情是不能出错的。

当人们研发芯片时，他们希望该芯片能够正常工作。当人们建造云基础设施时，他们不希望出现导致丢失数据的错误。那种精度很重要的应用程序需要非常严谨。你需要像 TLA+ 这样的东西，特别是系统中存在并发时，而这往往是常态。

程序员花在写代码上的时间比花在思考上的时间多，这是否是一种偏误？

是的，在编码前思考和撰写文档的重要性，需要在本科的计算机科学课程中教授。而现在却没有。原因是教编程的人和教程序验证的人之间没有沟通。

据我所知，双方都有责任。教编程的人不了解他们所需要的验证，教验证的人不了解如何在实践中进行应用。

在这个鸿沟被填平之前，TLA+ 是不会有大量用户的。我希望至少能让教授并发式编程的人明白他们需要它。那么也许就会有一些希望让 TLA+ 翻身。

我感觉到你对现在的计算机科学教育不太满意。是因为它对数学的重视程度不够吗？

是的，在数学思维方面。

那么，你将如何安排本科课程？

我不是一个教育者，所以不知道该如何教他们。但我知道人们应该学到什么。他们不应该害怕数学。这只是简单的数学，他们可能已经学过一门课程了，但不知道如何使用这些知识，不知道它有什么好处。他们只是学了点东西来通过考试，然后就把它忘了。

数学家们经常说他们在数学中看到了美。你是在这个领域起步的，那么你在算法中看的到美吗？

我不从美学的角度思考问题。我可能和其他人有同样的感觉，但只是用不同的词汇来表达它。美不是我对一个算法的评价。但是，简洁是我非常重视的东西。

最后一问，关于你的另一个具有相当大影响的副业项目：LaTeX。我想向创造者本人确认一下，它的发音是 LAH-tekh 还是 LAY-tekh？

随意。我不建议花太多时间考虑这个问题。

原文