LeslieLamport可能不是家喻户晓的名字，但对于计算机科学家来说，他是一些耳熟能详的“名字”背后的贡献者。比如Paxos算法、排版程序LaTeX、规范语言TLA+、“面包店算法”和“拜占庭一般问题”等等。LeslieLamport彻底改变了现代计算机相互通信的方式。2013年，他因在分布式系统方面的工作而获得图灵奖。在分布式系统中，不同网络上的多个组件协调以实现共同目标。互联网搜索、云计算和人工智能都需要许多强大的计算机协同工作。当然，这种配合也会让我们遇到更多的问题。Lamport曾经说过，“分布式系统是这样一种系统，其中一台您甚至不知道其存在的计算机出现故障，导致您自己的计算机无法使用。”最大的问题来源之一是“并发系统”，其中多个计算操作发生在重叠的时间片中，导致模棱两可：哪台计算机的时钟是正确的？在1978年的一篇开创性论文中，兰波特引入了“因果关系”的概念，利用狭义相对论的见解来解决这个问题。两个观察者可能不同意事件的顺序，但如果一个事件导致了另一个事件，那么歧义就解决了。发送或接收消息建立了多个进程之间的因果关系。“逻辑时钟”（现在也称为Lamport时钟）提供了一种对并发系统进行推理的标准方法。有了这个工具，计算机科学家开始思考如何系统地使这些连接的计算机变得更大而不增加错误。Lampor提出了一个优雅的解决方案：Paxos，一种允许多台计算机执行复杂任务的“共识算法”。如果没有Paxos及其算法家族，现代计算是不可能的。Paxos算法现在是一个行业标准。Lamport的另一个贡献是他在80年代初创建了文档准备系统LaTeX，为复杂的公式排版和科学文档格式化提供了成熟的方法。不仅在数学和计算机科学领域，在大多数科学领域，LaTeX已成为论文排版的标准。此外，Lamport开发的规范语言TLA+使工程师能够以精确的数学方式描述程序的目标。自1990年代以来，Lamport的工作重点是“形式验证”，即使用数学证明来验证软件和硬件系统的正确性。他的杰出贡献是创造了一种叫做TLA+（TemporalLogicofActions，行为的时间逻辑）的“规范语言”。软件规范就像一个程序的蓝图或配方，描述了软件应该如何在高层次上运行。这并不总是必要的，因为编写一个简单的程序就像煮鸡蛋一样。但是对于需要更高精度的更复杂、更冒险的任务，编写这样的程序就像准备九道菜的盛宴。你需要准备每道菜的每一个成分，以精确的方式组合它们，并以正确的顺序为每位客人提供服务。这需要精确的食谱和说明，用清晰简洁的语言编写，用英语散文写时可能会产生误导。TLA+使用精确的数学语言来防止错误并避免设计缺陷。将您的食谱或规格作为输入，一个称为模型检查器的程序会检查该食谱是否有意义并按预期工作以完全按照厨师的要求制作菜肴。在Lamport为程序员编写正确的规范之前，他感叹程序员经常将系统拼凑在一起，因为厨师无法在不知道他的食谱是否正确的情况下为晚宴准备食物。这些成就并非偶然。这位81岁的计算机科学家对人们如何使用和思考软件有着不同寻常的洞察力。Lamport最近接受了QuantaMagazine的采访，讨论了他在分布式系统方面的工作。在采访中，Lamport谈到了他创建的TLA+语言如何帮助程序员构建更好的系统，还谈到了当前计算机科学教育中存在的问题，强调了数学思维在计算机科学中的重要性。AI科技评论在不改变原意的情况下为读者整理了采访内容。图例：Lamport参观位于加利福尼亚州山景城的计算机历史博物馆Quanta：让我们从Paxos开始，因为它是一种非常有影响力的算法。您能谈谈是什么促使您开始从事这项工作吗？Lamport：当人们使用一些代码来构建系统时，我有一种预感，他们的代码试图实现的目标是不可能的。所以我决定尝试证明这一点，并想出了一个人们应该在他们的系统中使用的算法。Quanta：他们原来的算法有什么问题？Lamport：他们没有算法，他们只有一堆代码。很少有程序员从算法的角度来思考。在尝试编写并发系统时，如果只编写代码而没有算法，则程序将不可避免地充满错误。Quanta：介绍Paxos（“ThePart-TimeParliament”）的论文一开始并没有被广泛阅读。为什么？论文链接：https://dl.acm.org/doi/pdf/10.1145/279227.279229Lamport：原因可能是我喜欢用故事来解释事情，我用希腊字母来命名人物。例如，在论文中，有一位名叫ΓωИΔα的奶酪检查员。作为一个数学家，处处都是希腊字母，只是没想到非数学家也会被这些字母吓倒。这导致了这篇本应被看到而不被看到的论文。所以一开始Paxos的效果不是很好，但是从长远来看它确实达到了目的，因为人们把这一系列的共识算法叫做Paxos而不是“viewstampedreplication”（这是计算机科学家，对共识算法的另一种称呼）图灵奖得主芭芭拉·利斯科夫）。广达：在分布式系统领域研究了这么多年，是什么促使你开始创建TLA+？Lamport：在20世纪70年代，当人们对程序进行推理时，他们试图证明程序本身的属性，这些属性用编程语言表达。然后人们意识到他们真的应该首先说明程序试图完成什么——即程序的行为。在80年代初期，我意识到为并发系统编写这些高级规范的一种实用方法是将它们编写为抽象算法。使用TLA+，我能够以足够严格的方式在数学上表达它们。事实证明，TLA+做得很好。重要的是不要试图用编程语言编写算法：如果你真的想把事情做好，你需要用数学术语来编写你的算法。广达：您曾经说过，“如果你思考而不写作，你只会思考你所想的。”那是模型检查的目的吗？Lamport：模型检查是一种全面测试系统小模型的所有实现的方法。它只说明模型的正确性，不说明算法的正确性。虽然模型检查是为了验证正确性，但编码只是生成代码，它不会测试任何东西。在模型检查之前，确保算法有效的唯一方法是编写证明。实际上，模型检查检查算法的一个小实例的所有执行。如果幸运的话，您将能够检查足够多的实例，从而对您的算法有足够的信心。但是对于任何规模的系统和算法的使用，证明都可以验证它们的正确性。Quanta：听起来模型检查与另一种程序验证方法有关：使用Coq等工具进行交互式定理证明。它们有何不同？Lamport：Coq的目的是解决真正的数学问题，它能够捕捉到数学家所做的推理。例如，GeorgesGonthier用它来证明四色定理。当一个数学命题的证明被机器验证后，几乎可以肯定这个命题是正确的。TLA+不是为数学家设计的，而是为希望证明其系统特性的工程师设计的。在1990年代，在花了大约15年编写并发算法的证明之后，我了解了如何证明并发算法的正确性。TLA是一种可以将证明过程完全形式化的逻辑，TLA+也是一种完全基于TL逻辑的语言。广达：像TLA+这样的规范语言在工业上应用并不广泛，是吗？你为什么认为这是？兰波特：我正在尽力而为。但基本上，程序员和许多（如果不是大多数的话）计算机科学家都被数学吓倒了。所以它的“营销”难度很大。另外，每个项目都必须匆忙完成。有句老话说：“时间永远不够完美地做一件事，但总有时间重新做。”由于TLA+涉及前期工作，在开发过程中增加了新的步骤，这也导致其应用不广泛。Quanta：前期的工作总是值得的吗？Lamport：的确，世界各地的程序员编写的大多数代码都不需要非常精确地说明它应该做什么。但是有些事情很重要才能正确。例如，当人们制造芯片时，他们希望它们能工作。当人们构建云基础设施时，他们不希望出现丢失人们数据的错误。对于需要精度的应用程序，您需要非常严格。你需要像TLA+这样的东西，尤其是当涉及到通常存在于这些系统中的并发性时。Quanta：程序员写代码的时间是否往往比思考代码的时间多？Lamport：是的，需要在本科计算机科学课程中教授在编写代码之前思考和编写的重要性，但事实并非如此。原因是教编程的人和教程序验证的人之间没有交流。据我所知，这个鸿沟的两边都存在问题。教编程的人不了解他们需要了解的有关验证的知识，而教验证的人不了解它应该如何在实践中应用和使用。在弥合这一差距之前，TLA+不会获得大量用户。我希望我至少可以让教并发编程的人明白他们需要TLA+。那样的话，TLA+或许就有希望被更多人使用。Quanta：我感觉你对这几年的计算机教育不是很满意。是因为对数学不够重视吗？Lamport：是的，就数学思维而言。Quanta：那么，你会如何安排你的本科课程？Lamport：我不是教育家，所以我不知道如何教他们。但我知道人们应该学习什么。他们不应该害怕数学。他们可能已经学会了简单的数学，但不知道如何使用它。他们不知道这有什么好处。他们学得够多，通过了考试，就忘掉了。Quanta：数学家常说他们在数学中看到了美。你是从算法领域起家的，那么你见过算法之美吗？Lamport：我不从美学角度考虑。我可能和其他人有同样的感觉，但我只是用不同的语言来表达。关于算法，我不考虑美，简单是我非常看重的东西。
