专访分布式系统奠基人之一，图灵奖得主 Leslie Lamport ：思考比编码重要

转载请微信联系：huangdiezi，更多DAO、Web3、NFT、Metaverse资讯请关注老雅痞👇

信息来源：Quanta

Leslie Lamport可能并不是一个家喻户晓的名字，但对于计算机科学家们来说，他是一些耳熟能详的「名字」幕后的贡献者。比如Paxos算法、排版程序LaTeX、规格语言TLA+、「面包店算法」和「拜占庭将军问题」等等。

这位81岁的计算机科学家对人们如何使用和思考软件有着不同寻常的思考。

 

2013年，他因其在分布式系统方面的工作而获得了被认为是计算界诺贝尔奖的图灵奖（A.M. Turing Award），其中不同网络上的多个组件相互协调以实现一个共同目标。互联网搜索、云计算和人工智能都涉及协调强大的计算机器军团一起工作。当然，这种协调会遇到更多问题。

 

Lamport曾经说过："分布式系统是这样一种系统，在这种系统中，一台你甚至不知晓其存在的计算机出现了故障，就会导致你自己的计算机无法使用。”

 

其中最大的问题来源是 "并发系统"，其中多个计算操作发生在重叠的时间片上，导致了模糊不清的情况。哪台计算机的时钟是正确的？在1978年的一篇开创性的论文中，Lamport引入了 "因果关系 "的概念来解决这个问题，使用的是狭义相对论的一个见解。两个观察者可能对事件的顺序有异议，但如果一个事件导致另一个事件，这就消除了模糊性。而发送或接收一个信息可以在多个过程中建立因果关系。逻辑时钟--现在也称为Lamport时钟--提供了一种推理并发系统的标准方法。

 

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

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

 

自20世纪90年代以来，Lamport的工作重点是形式验证，即使用数学证明来验证软件和硬件系统的正确性。值得注意的是，他创造了一种名为TLA+（行动的时间逻辑）的规范语言。软件规范就像一个程序的蓝图或食谱；它描述了软件在高层次上应该如何表现。这并不是必要的，因为给一个简单的程序编码就像煮鸡蛋一样。但是，一个更复杂的任务有更大的风险--编码相当于制作一个九道菜的宴会需要更多的精度。你需要准备每道菜的每个组成部分，以精确的方式组合它们，然后以正确的顺序将它们端给每一位客人，这需要准确的食谱和说明，用毫不含糊和简洁的语言编写，但用英语散文编写的描述可能会留下误解的空间。TLA+采用了精确的数学语言来防止bug和避免设计缺陷。

 

使用你的食谱或规范作为输入，一个被称为模型检查器的程序将检查食谱是否有意义，是否按照预期的方式工作，按照厨师想要的方式制作菜肴。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+是不会找到大量的用户的。我希望我至少可以让教授并发编程的人明白他们需要它。那么也许就会有一些希望。

 

我感觉到，你对现在的计算机科学教育不太满意。是不是因为它对数学强调得不够？

在数学思维方面，是的。

 

那么，你将如何构建一个本科课程？

 

我不是一个教育家，所以我不知道如何教给他们。但我知道人们应该学到什么，他们不应该害怕数学。这只是简单的数学，他们可能已经学过一门课程，但他们不知道如何使用它，他们不知道它有什么好处。

 

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

 

我不从美学的角度考虑。我可能有其他人的那种感觉，但我只是用不同的词来表达它们。美丽不是我对算法的评价，但是简单性是我非常重视的。