编辑 | 白菜叶Leslie Lamport 可能不是一个家喻户晓的名字，但他是其中一些计算机科学家的幕后推手：排版程序 LaTeX 以及使 Google 和 Amazon 的云基础设施成为可能的工作。
他还对一些问题给予了更多关注，给它们起了独特的名字，比如面包店算法和拜占庭将军问题。
这绝非偶然。
这位 81 岁的计算机科学家对人们如何使用和思考软件有着不同寻常的深思熟虑。
2013 年，他赢得了被认为是计算领域诺贝尔奖的图灵奖，表彰了他在分布式系统方面的工作，其中包括不同网络上的多个组件相互协调以实现共同目标。
互联网搜索、云计算和人工智能都涉及编排强大的计算机军团协同工作。
当然，这种协调会给你带来更多的问题。
「分布式系统是一个你甚至不知道存在的计算机的故障，可能导致你自己的计算机无法使用的系统。
」Lamport 曾经说过。
问题的最大来源之一是「并发系统」，其中多个计算操作发生在重叠的时间片中，导致模棱两可：哪台计算机的时钟是正确的？在 1978 年的一篇开创性论文中，Lamport 利用狭义相对论的见解引入了「因果关系」的概念来解决这个问题。
两个观察者可能在事件的顺序上存在分歧，但如果一个事件导致另一个事件，这就消除了歧义。
并且发送或接收消息可以在多个进程之间建立因果关系。
逻辑时钟——现在也称为 Lamport 时钟——提供了一种推理并发系统的标准方法。
论文链接：https://dl.acm.org/doi/10.1145/359545.359563有了这个工具，计算机科学家接下来想知道他们如何系统地使这些连接的计算机变得更大，而不会增加错误。
Lamport 提出了一个优雅的解决方案：Paxos，一种允许多台计算机执行复杂任务的「共识算法」。
如果没有 Paxos 及其算法家族，就不可能存在现代计算。
在 1980 年代初期，随着他开发该领域，Lamport 还创建了 LaTeX，这是一个文档准备系统，它提供了复杂的方法来排版复杂的公式和格式化科学文档。
LaTeX 已成为格式化论文的标准，不仅在数学和计算机科学领域，而且在大多数科学领域也是如此。
Lamport 自 1990 年代以来的工作重点是「形式验证」，即使用数学证明来验证软件和硬件系统的正确性。
值得注意的是，他创建了一种名为 TLA+（用于 Temporal Logic of Actions）的「规范语言」。
软件规范就像程序的蓝图或配方；它描述了软件在高层次上的行为方式。
这并不总是必要的，因为编写一个简单的程序类似于煮鸡蛋。
但更复杂、风险更高的任务——相当于九道菜宴会的编码——需要更高的精度。
你需要准备好每道菜的每个成分，以精确的方式将它们组合在一起，然后以正确的顺序将它们提供给每位客人。
这需要准确的食谱和说明，以明确和简洁的语言编写，但用英语散文编写的描述可能会留下误解的空间。
TLA+ 采用精确的数学语言来防止错误并避免设计缺陷。
使用你的食谱或规格作为输入，称为模型检查器的程序将检查食谱是否有意义并按预期工作，以厨师想要的方式制作菜肴。
Lamport 感叹程序员如何在编写适当的规范之前经常拼凑一个系统，而厨师永远不会在不知道他们的食谱是否有效的情况下准备宴会。
媒体与 Lamport 讨论了他在分布式系统方面的工作、计算机科学教育出了什么问题，以及使用 TLA+ 如何帮助程序员构建更好的系统。
Q：让我们从 Paxos 开始，因为它是如此有影响力的算法。
是什么让你首先开始研究它？A：人们正在用一些代码构建一个系统，我有预感，他们的代码试图完成的事情是不可能的。
因此，我决定尝试证明这一点，而是提出了一种人们应该在他们的系统中使用的算法。
Q：他们原来的算法有什么问题？A：好吧，他们没有算法，只有一堆代码。
很少有程序员从算法的角度思考。
在尝试编写并发系统时，如果你只是编写代码而不使用算法，那么你的程序就不会充满错误。
Q：介绍 Paxos 的论文起初并没有被广泛阅读。
那是为什么？论文链接：https://dl.acm.org/doi/10.1145/279227.279229使人们无法阅读这篇论文的原因是我喜欢用故事来解释事物，并且我用某种伪希腊字母为角色命名。
例如，论文中提到过一位名叫 Γωυδα 的奶酪检查员。
作为一名数学家长大，希腊字母到处都是，我只是不知道非数学家完全被这些字母吓坏了。
显然，读者无法处理它，这导致该论文没有按应有的方式阅读。
所以一开始效果并不好。
尽管从长远来看确实如此，因为人们将这一系列共识算法称为 Paxos，而不是「viewstamped replication」，后者是 [计算机科学家] Barbara Liskov 对同一算法的另一个名称。
Q：从事分布式系统多年，是什么让你进入 TLA+？A：在 1970 年代，当人们对程序进行推理时，他们正在证明程序本身以编程语言的形式表述的属性。
然后人们意识到他们真的应该先说明程序应该首先完成什么——程序的行为。
在 1980 年代初期，我意识到为并发系统编写这些高级规范的一种实用方法是将它们编写为抽象算法。
使用 TLA+，我能够以完全严谨的方式在数学上表达它们。
一切都点击了。
这涉及的基本上不是试图用编程语言编写算法：如果你真的想把事情做好，你需要用数学的方式来编写你的算法。
Q：你说过，「如果你在思考而不写作，你只会认为你在思考。
」 这就是模型检查的用武之地吗？A：模型检查是一种详尽地测试系统小模型的所有执行的方法。
它只是显示模型的正确性，而不是算法的正确性。
在模型检查测试正确性时，编码只是产生代码。
它不测试任何东西。
在进行模型检查之前，确保你的算法有效的唯一方法是编写证明。
在实践中，模型检查检查算法的一个小实例的所有执行。
如果幸运的话，你可以检查足够大的实例，从而使你对算法有足够的信心。
但是这个证明可以证明它对于任何规模的系统和算法的任何使用都是正确的。
Q：听起来模型检查与另一种程序验证方法有关：使用 Coq 等工具进行交互式定理证明。
它们有何不同？A：Coq 旨在进行真正的数学运算，并能够捕捉数学家所做的推理。
例如，Georges Gonthier 就是用它来证明四色定理。
数学陈述的机器检查证明表明该陈述几乎肯定是正确的。
TLA+ 不是为数学家设计的，而是为想要证明其系统属性的工程师设计的。
在 1990 年代，在花了大约 15 年时间编写并发算法的证明之后，我了解到你需要做什么才能证明并发算法的正确性。
TLA 是允许它完全正式的逻辑。
TLA+ 是基于此的完整语言。
Q：像 TLA+ 这样的规范语言在工业中并没有被广泛使用，对吧？你认为这是为什么？A：好吧，我正在做我能做的。
但基本上，程序员和许多（如果不是大多数）计算机科学家都被数学吓坏了。
所以这是一个艰难的销售。
其次，每个项目都必须匆忙完成。
有句老话：「从来没有时间做正确的事。
总有时间再做一遍。
」 因为 TLA+ 涉及前期工作，所以你在开发过程中添加了一个新步骤，这也是一个很难的推销。
Q：是否总是值得预先付出努力？A：诚然，全世界程序员编写的大多数代码都不需要非常精确地说明它应该做什么。
但是有些事情很重要，需要正确。
当人们构建芯片时，他们希望该芯片能够正常工作。
当人们构建云基础设施时，他们不希望出现会丢失人们数据的错误。
对于精度很重要的应用程序，你需要非常严格。
你需要像 TLA+ 这样的东西，尤其是在涉及并发的情况下，这些系统中通常会有这种情况。
Q：程序员在编写代码上花费的时间比他们思考的时间多吗？A：是的，在编写代码之前思考和写作的重要性需要在本科计算机科学课程中教授，但事实并非如此。
原因是教编程的人和教程序验证的人之间没有交流。
从我所看到的情况来看，问题出在分歧的两边。
教编程的人不知道他们需要知道的验证。
教授验证的人不明白它应该如何在实践中应用和使用。
在弥合这一鸿沟之前，TLA+ 不会找到大量用户。
我希望我至少能让教授并发编程的人明白他们需要它。
那么也许还有希望。
Q：感觉你现在对计算机科学教育不太满意。
是因为它没有对数学给予足够的重视吗？A：关于数学思维，是的。
Q：那么，你将如何构建本科课程呢？A：我不是教育工作者，所以我不知道如何教他们。
但我知道人们应该学到什么。
他们不应该害怕数学。
这只是简单的数学，他们可能已经上过一门课程，但他们不知道如何使用它。
他们不知道这有什么好处。
他们学到了足够的知识来通过考试，然后他们就忘记了。
Q：数学家经常说他们看到了数学的美。
你是从那个领域开始的，所以你看到算法的美吗？A：我不考虑美学。
我可能有其他人的那种感觉，但我只是用不同的词来表达它们。
对于算法，我不会说美丽。
但简单是我非常看重的东西。
Q：最后一件事，关于你的另一个具有相当大影响的副项目：LaTeX。
我想最终与创作者澄清一些事情。
它的发音是 LAH-tekh 还是 LAY-tekh？A：随心所欲。
我不建议花太多时间考虑它。
相关报道：https://www.quantamagazine.org/computing-expert-says-programmers-need-more-math-20220517/