2013年图灵奖得主 Leslie Lamport 专访：程序员需要更多的数学知识

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

Leslie Lamport 彻底改变了现代计算机之间的对话方式。2013年，他被授予图灵奖，以表彰他在分布式系统方面的工作。

在分布式系统中，不同网络上的多个组件协调一致，以实现一个共同的目标。互联网搜索、云计算和人工智能都需要协调众多强大的计算机器协同工作。当然，这种协调也会使我们遇到更多的问题。

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

最大的问题来源之一是「并发系统」，即在重叠的时间片段内发生多个计算操作，这导致了一种模糊性：哪台计算机的时钟是正确的？在1978年的一篇开创性论文中，Lamport引入了「因果关系」的概念，利用狭义相对论的观点来解决这个问题。两个观察者在事件顺序上可能存在分歧，但如果是一个事件导致另一个事件的发生，那么就能消除模糊性。发送或接收消息可以在多个进程之间建立因果关系。「逻辑时钟」（现在也被称为Lamport时钟），提供了一种标准的方法来对并发系统进行推理。

有了这个工具以后，计算机科学家开始想知道他们如何系统地将这些连接的计算机变得更大，而不增加Bug。Lampor提出了一个优雅的解决方案：Paxos，一种允许多台计算机执行复杂任务的「一致性算法」。没有Paxos及其算法家族，现代计算就不可能存在。Paxos算法现在已经成为行业标准。

Lamport的另一贡献，是他在上世纪80年代初创建了文档准备系统LaTeX，提供了复杂公式排版和科学文档格式的复杂方法。不仅在数学和计算机科学领域，而且在大多数科学领域，LaTeX已经成为论文格式的标准。

另外，Lamport所开发的规格语言TLA+使得工程师能够以一种精确的、数学的方式描述程序的目标。自20世纪90年代以来，Lamport的工作就一直专注于「形式验证」（formal verification），即使用数学证明来验证软件和硬件系统的正确性。他的突出贡献便是创建了一种「规格语言」，称为TLA+（Temporal Logic of Actions，行为时序逻辑）。软件规格说明就像一个程序的蓝图或配方，它描述软件应该如何在高层次上运行。这并不总是必要的，因为编写一个简单的程序就像煮一个鸡蛋一样。但若是一项更复杂、风险更高的任务，则需更高的精确度，编写这样一个程序就相当于准备一场九道菜的盛宴。你需要准备每道菜的每个组成部分，以一种精确的方式组合它们，然后按照正确的顺序把它们端给每一位客人。这需要精确的食谱和说明，并以明确简洁的语言来书写，而描写成英语散文，则可能会导致误解。TLA+使用精确的数学语言来防止错误和避免设计缺陷。

将你的菜谱或规格作为输入，一个叫做模型检查器的程序会检查菜谱是否合理、是否按预期工作，从而按照厨师的要求做出一道菜。在Lamport为程序员编写适当的规格以前，程序员们经常胡乱拼凑一个系统，这曾让他感到惋惜，毕竟厨师在不知道自己的食谱是否正确的情况下，是无法为宴会准备食物的。

这些成就并不是偶然的。这位81岁的计算机科学家对于人们如何使用和思考软件有着不同寻常的见解。

最近，Quanta Magazine对Lamport进行了一次专访，讨论了他在分布式系统方面的工作。在采访中，Lamport谈论了他所创建的TLA+语言如何帮助程序员构建更好的系统，还谈及了当前计算机科学教育中存在的问题，强调了数学思维在计算机科学中的重要性。

AI科技评论在不改变原意的基础上对该专访进行了编译，以飨读者。

图注：Lamport参观加州山景城的计算机历史博物馆

Quanta：我们先从Paxos谈起，因为它是一个非常有影响力的算法。能否谈谈是什么驱动您开始做这项工作的？

Lamport：当时人们使用一些代码去构建一个系统，我有种预感，他们的代码所试图实现的目标是不可能的。因此，我决定尝试去证明这一点，并提出了一种人们应该在他们的系统中使用的算法。

Quanta：他们原有的算法存在什么问题？

Lamport：他们并没有算法，而是只有一堆代码。很少有程序员用算法来思考问题。在尝试编写并发系统时，如果只编写代码而没有算法，那么你的程序必然会到处都是bug。

Quanta：介绍Paxos的那篇论文（“The Part-Time Parliament”）起初并没有被广为阅读。为什么会这样？

论文链接：https://dl.acm.org/doi/pdf/10.1145/279227.279229

Lamport：原因可能是我喜欢用故事来解释事情，而且我用希腊字母来为人物命名。例如，在论文中，有一位奶酪检查员名叫ΓωИΔα。身为一名数学家，在这里随处可见希腊字母，我只是没有意识到那些不是数学家的人会被这些字母给吓到。这导致了这篇原本应该被看见的论文而没有被看见。

所以在一开始Paxos的应用效果并不太好，但从长远来看它的确实现了它的目标，因为人们称这一系列的共识算法为Paxos，而不是「viewstamped replication」（这是计算机科学家、图灵奖得主Barbara Liskov对共识算法的另一个命名）。

Quanta：在分布式系统领域研究了这么多年之后，是什么让您开始了创建TLA+的工作？

Lamport：在20世纪70年代，当人们对程序进行推理时，他们试图证明程序本身的属性，这些属性是用编程语言表述的。后来人们意识到，他们确实应该说明程序首先要完成什么——即程序的行为。

在20世纪80年代初，我意识到，为并发系统编写这些更高级别规格的实用方法，是将它们编写为抽象的算法。有了TLA+，我就能够以一种足够严谨的方式用数学去表达它们。后来证明，TLA+的确做得很出色。重要的是，不要试图用编程语言来编写算法：如果你真的想把事情做好，你需要用数学的术语来编写你的算法。

Quanta：您曾说过，「如果你只思考而不写作，你就只会思考你在思考的东西。」这就是模型检测（model checking）的目的吗？

Lamport：模型检测是一种全面检测系统小模型的所有执行情况的方法。它只显示模型的正确性，而不是算法的正确性。当模型检测去验证正确性时，编码只会生成代码，它不测试任何东西。在进行模型检测之前，确保算法有效的唯一方法是写证明（proof）。

在具体实践中，模型检测会检查算法的一个小实例的所有执行情况。如果幸运的话，您可以检查足够多的实例，从而使你对算法有足够的信心。但对于任何规模的系统和算法的使用，证明都可以验证其正确性。

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

Lamport：Coq的目的是解决真正的数学问题，它能够捕捉数学家所做的推理。例如， Georges Gonthier用它来证明了四色定理（four-color theorem）。一个数学命题的证明经过机器验证后，几乎可以肯定该命题为真。

TLA+不是为数学家设计的，而是为希望证明其系统特性的工程师设计的。20世纪90年代，在花了大约15年的时间编写并发算法的证明之后，我了解到为了证明并发算法的正确性需要做什么。TLA是能够一种让证明过程具有完全的形式化的逻辑，而且TLA+也是基于TL逻辑的一套完整语言。

Quanta：像TLA+这样的规范语言在工业中使用得不是很广泛，是吗？您认为这是为什么？

Lamport：我正在尽我所能。但基本上，程序员和许多（如果不是大多数的话）计算机科学家都被数学给吓坏了。所以它的「销路」很困难。

另外，每个项目都必须急匆匆地赶完。有句老话，「永远没有足够的时间把一件事做到完美，但总是有时间去重新来过。」因为TLA+涉及到前期工作，在开发过程中又会添加新步骤，所以这也导致了它没有被广泛使用。

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

Lamport：的确，世界各地的程序员编写的大多数代码都不需要非常精确的语句来说明它应该做什么。但有些事情很重要，需要保证正确。

例如，当人们制造芯片时，他们希望芯片能正常工作。当人们构建云基础设施时，他们不希望出现会丢失人们数据的bug。对于那些要求精度的应用程序，你需要非常严格。而且你需要类似于TLA+的东西，尤其是当涉及到通常存在于这些系统中的并发时。

Quanta：程序员是否倾向于花更多的时间去写代码而非思考代码？

Lamport：是的，在编写代码之前进行思考和写作的重要性，需要在本科的计算机科学课程中教授，但事实并非如此。原因是教编程的人和教程序验证的人之间没有交流。

就我所见，这一分歧的两边都存在问题。教编程的人不了解他们需要知道的验证，而教授验证的人不理解它应该如何应用和在实践中使用。

在弥合这一鸿沟之前，TLA+是不会收获大量用户的。我希望我至少能让教授并发编程的人明白他们需要TLA+。那样的话，TLA+也许还有希望被更多人使用。

Quanta：我感觉到，您对近年来的计算机科学教育不太满意。是不是因为对数学重视不够？

Lamport：是的，在数学思维方面。

Quanta：那么，您会如何构建本科课程？

Lamport：我不是一个教育家，所以我不知道如何教他们。但我知道人们应该学到什么。他们不应该害怕数学。他们可能学过一门简单的数学，但不知道如何使用它。他们不知道这有什么好处。他们学了足够多的知识，通过了考试，然后就抛之脑后。

Quanta：数学家常说他们在数学中看到了美。你是从算法领域起步的，那么您看到算法之美了吗？

Lamport：我并不从美学的角度来考虑。我可能和其他人有同样的感觉，但我只是用不同的语言来表达。关于算法，我考虑的不是美，简单是我非常看重的东西。