# 如何用完美的数学方法编写软件 By [SeeDAO](https://paragraph.com/@seedao) · 2022-08-05 --- _【摘要】数学家出身的 Leslie Lamport 也是杰出的计算机科学家，LaTex、逻辑时钟，以及对分布式系统至关重要的 Paxos 共识算法都是他的手笔。Lamport 强调规范语言对于复杂系统开发的重要性，并为之开发了 TLA+。由于在分布式系统领域作出的突出贡献，Lamport 获得了图灵奖。_ _【标签】#计算机历史 #人物 #分布式计算 #Paxos #LaTeX #TVL+_ _【题图】Talia Herman for Quanta Magazine_ _作者：_[_Sheon Han_](https://www.quantamagazine.org/authors/sheon-han/)_｜译者：常真｜校对：_[_Roy_](https://twitter.com/MroyBB)_｜排版：_[_Queeny_](https://twitter.com/Queeny_TWP) * * * **_Leslie Lamport 彻底改变了计算机之间的对话方式。现在他正在研究工程师如何与他们的机器对话。_** 由于计算机科学家 Leslie Lamport 的工作，现代计算机可以有效地相互协同。此后，他将注意力转向了如何让编程本身更有效率。 * * * [Leslie Lamport](http://www.lamport.org/) 也许不是一个家喻户晓的名字，但计算机科学家知道，排版系统 LaTeX 和让谷歌和亚马逊云基础设施得以实现的技术的背后都有他的身影。他还给几个问题起了独特的名字，让人们更加关注，如面包房算法和拜占庭将军问题。这绝非偶然。这位 81 岁的计算机科学家，对人们如何使用和思考软件有着不同寻常的想法。 2013 年，他获得了图灵奖（计算机领域的诺贝尔奖），表彰他在分布式系统方面的工作。分布式系统让不同网络上的多个组件相互协同来实现共同目标。互联网搜索、云计算和人工智能都涉及协同很多强大的计算机器一起工作。当然，这种协同会让你遇到更多的问题。 Lamport 曾经说过：“在分布式系统中，一台你甚至都不知道的计算机发生了故障，就能让你自己的计算机无法使用。” 最大的麻烦中有一个是 ＂并发系统＂，即在相互重叠的时间片段内发生多个计算操作，导致了二义性。哪台计算机的时钟是正确的？在 1978 年的一篇开创性的论文中，Lamport 借用狭义相对论的见解，引入了＂因果关系＂的概念来解决这个问题。两个观察者可能对事件的顺序有异议，但如果一个事件导致了另一个事件的发生，就消除了二义性。发送或接收一条信息可以在多处理中建立因果关系。逻辑时钟——现在也被称为 Lamport 时钟——提供了一种并发系统推算的标准方法。 有了这个工具，计算机科学家接下来想知道，他们如何能够系统性地扩大相互连接的计算机，而不增加错误。Lamport 想出了一个优雅的解决方案：Paxos，一种允许多台计算机执行复杂任务的 "共识算法"。没有 Paxos 和它的系列算法，现代计算机系统就不可能存在。 Talia Herman 拍摄 20 世纪 80 年代初，在拓展该领域的同时，Lamport 还创建了 LaTeX。这是一个文件预处理系统，为复杂公式的排版和格式化科学文献提供了精巧的方法。不仅在数学和计算机科学领域，LaTeX 在大多数科研领域都已成为论文的格式标准。 自 20 世纪 90 年代以来，Lamport 将工作重点转向了＂形式验证＂，即使用数学证明来验证软件和硬件系统的正确性。值得注意的是，他创造了一种名为 [TLA+](https://lamport.azurewebsites.net/tla/tla.html)（Temporal Logic of Actions，行为时序逻辑）的 "规范语言"。软件规范就像程序的蓝图或食谱；它描述了软件在高层次上应该如何表现。这并不总是必要的，因为编写简单的程序就跟煮鸡蛋差不多。但是，更加复杂的高风险任务对精确度的要求也更高——此时的编码工作相当于烹制满汉全席。你需要为每道菜备好食材，精心配制，再分毫不差地端上桌给供位客人享用。这就要用到以简练明晰的语言写成的正确食谱和烹饪说明了，而用英语随意写出来的描述就可能会造成误解。TLA+ 采用精确的数学语言来防止错误，避免设计缺陷。 使用食谱或规范作为输入，一个被称为模型检测器的程序将检查食谱是否合理，是否能够按照预期来工作，按照厨师的要求制作出菜肴。Lamport 感叹程序员经常在写出适当规范之前就拼凑出一个系统，然而，厨师们在不知道食谱是否有效的情况下，可不会答应承办宴会的。 _Quanta_（_译注：发表本文的杂志_）与 Lamport 谈了他在分布式系统方面的工作，计算机科学教育出现的问题，以及如何使用 TLA+ 帮助程序员开发更好的系统。为使文意清晰，采访内容经过了精简和编辑。 ### 让我们先聊聊 Paxos 这个非常有影响力的算法。起初是什么让你开始研究它的？ 那时人们正在用一些代码来开发系统，而我有一种预感，他们的代码不可能实现预期目标。因此，我决定尝试证明这一点，结果想出了一个算法。这个算法本来就应该在人们的系统中使用。 ### 他们的原始算法有什么问题？ 嗯，他们没有算法，只有一堆代码。很少有程序员用算法来思考问题。当你试图编写一个并发系统时，如果在没有算法的情况下写代码，你的程序就不可能没有一堆错误。 Lamport 参观位于加州山景城的计算机历史博物馆。Talia Herman 拍摄 ### 介绍 Paxos 的论文起初并没有广泛传播，为什么？ 人们阅读[那篇论文](https://dl.acm.org/doi/10.1145/279227.279229)有困难的原因是，我喜欢用故事来解释事情，而且会用某种伪希腊字母为故事里的人物起名字。比如这篇论文中，有一个名叫 Γωυδα 的奶酪质检员。作为一名数学家，我天天跟希腊字母打交道，只是不知道别人会被这些字母吓坏。很明显，读者不吃这一套，于是那篇论文没有得到应有的阅读量。 所以一开始它的阅读量不佳。虽然长期来看它得到了应有的重视，但那也是因为人们给这套共识算法起了个好名字：Paxos，而不是＂Viewstamped Replication＂，后者是计算机科学家 [Barbara Liskov](https://www.quantamagazine.org/barbara-liskov-is-the-architect-of-modern-algorithms-20191120/) 同一算法的另一个名称。 ### 在分布式系统方面工作了这么多年，是什么让您转而开发 TLA+ ？ 在 20 世纪 70 年代，人们对程序进行探究，试图用编程语言来证明程序自身的属性。后来，人们意识到应该首先说明程序应该完成什么——也就是程序的行为。 20 世纪 80 年代初，我意识到，为并发系统编写这些更高级规范的实用方法，是把它们写成抽象的算法。有了 TLA+，我就能以一种非常严谨的数学方式来表达它们，然后就一切都合拍了。这里讲的是，不要试图用编程语言来写算法。如果真的想把事情做好，你需要用数学语言来写算法。 Lamport 说：“在写代码前先思考和撰写文档的重要性，需要在本科的计算机科学课程中教授，而现在并没有。” Talia Herman 拍摄 ### 你说过，"如果只思考不撰写文档，那你只是自以为是"。这就是模型检测的作用吗？ 模型检测是一种测试方法，它会对系统模型的所有执行进行穷尽测试。它只说明模型的正确性，而不是算法的正确性。当模型检测对正确性进行测试时，编码只是生成代码，它并不测试任何东西。在模型检测出现之前，确保算法有效的唯一方法是写出证明。 在实践中，模型检测会检查算法实例的所有执行情况。如果你很幸运，可以检查足够多的实例，让你对该算法更有把握。但是，对于任何规模的系统和算法的任何运用，这个证明都可以验证其正确性。 ### 听起来，模型检测与另一种程序验证方法有关：使用 Coq 等工具进行交互式定理证明。它们有什么不同？ Coq 是专为解决数学问题设计的，并且能够采集记录数学家所做的推理。例如，Georges Gonthier 就是用它来证明[四色定理](https://www.quantamagazine.org/decades-old-graph-problem-yields-to-amateur-mathematician-20180417/)的。一个数学命题的证明经过机器验证后，几乎可以肯定该命题为真。 TLA+ 不是为数学家设计的，而是为那些想证明系统属性的工程师设计的。20 世纪 90 年代，在花了大约 15 年时间编写并发算法的证明之后，我学会了为证明并发算法的正确性需要做什么。TLA 是一种逻辑，它能让所有的证明过程具有完备的形式化逻辑。而 TLA+ 则是基于此的一套完整语言。 Lamport 获得了 2013 年的图灵奖，表彰他在分布式系统领域计算机协同方面的工作。他的 Paxos 算法现在已成为行业标准。 Talia Herman 拍摄 ### 像 TLA+ 这样的规范语言在业界的应用并不广泛，对吗？你认为这是为什么呢？ 好吧，[我正在尽自己的一份力](https://www.youtube.com/channel/UCajiu4Cj_GHOX0if3Up-eRA)。但基本上程序员和许多（如果不是大多数）计算机科学家都被数学吓坏了。所以它很难推广。 第二，每个项目都要匆匆完成。有一句老话，"永远没有时间把事儿做对，但总有时间重新来过。"因为 TLA+ 涉及前期工作，相当于在开发过程中增加了一个新的步骤，这也让它的采用变得困难。 ### 前期的工作是否总是值得？ 诚然，世界各地的程序员所写的大部分代码，确实不需要非常精确的文档来说明它应该如何运行。但是，有些非常重要的事情是不能出错的。 当人们研发芯片时，他们希望该芯片能够正常工作。当人们建造云基础设施时，他们不希望出现导致丢失数据的错误。那种精度很重要的应用程序需要非常严谨。你需要像 TLA+ 这样的东西，特别是系统中存在并发时，而这往往是常态。 由 Lamport 在过去几十年中开发的规范语言 TLA+，允许工程师以精确的数学方式描述程序的目标。Talia Herman 拍摄 ### 程序员花在写代码上的时间比花在思考上的时间多，这是否是一种偏误？ 是的，在编码前思考和撰写文档的重要性，需要在本科的计算机科学课程中教授。而现在却没有。原因是教编程的人和教程序验证的人之间没有沟通。 据我所知，双方都有责任。教编程的人不了解他们所需要的验证，教验证的人不了解如何在实践中进行应用。 在这个鸿沟被填平之前，TLA+ 是不会有大量用户的。我希望至少能让教授并发式编程的人明白他们需要它。那么也许就会有一些希望让 TLA+ 翻身。 ### 我感觉到你对现在的计算机科学教育不太满意。是因为它对数学的重视程度不够吗？ 是的，在数学思维方面。 ### 那么，你将如何安排本科课程？ 我不是一个教育者，所以不知道该如何教他们。但我知道人们应该学到什么。他们不应该害怕数学。这只是简单的数学，他们可能已经学过一门课程了，但不知道如何使用这些知识，不知道它有什么好处。他们只是学了点东西来通过考试，然后就把它忘了。 ### 数学家们经常说他们在数学中看到了美。你是在这个领域起步的，那么你在算法中看的到美吗？ 我不从美学的角度思考问题。我可能和其他人有同样的感觉，但只是用不同的词汇来表达它。美不是我对一个算法的评价。但是，简洁是我非常重视的东西。 ### 最后一问，关于你的另一个具有相当大影响的副业项目：LaTeX。我想向创造者本人确认一下，它的发音是 LAH-tekh 还是 LAY-tekh？ 随意。我不建议花太多时间考虑这个问题。 * * * 原文 [ Computing Expert Says Programmers Need More Math | Quanta Magazine ------------------------------------------------------------------ Leslie Lamport revolutionized how computers talk to each other. Now he's working on how engineers talk to their machines. https://www.quantamagazine.org ![](https://storage.googleapis.com/papyrus_images/1d9f36ea921995940eab8205534ed2263c85a6bf03779408a1cd1dc7f32b5006.jpg) ](https://www.quantamagazine.org/computing-expert-says-programmers-need-more-math-20220517) * * * ![](https://storage.googleapis.com/papyrus_images/e9594f6c714b0ca4af70dac7d7e2c3721233cb54ccebecfc52624c465c938d7d.png) --- *Originally published on [SeeDAO](https://paragraph.com/@seedao/SXwOIQ3ayZkF7VaPlPLG)*