2013年图灵奖得主Leslie Lamport：如何写出数学上完美的算法

来源：新智元
本文约3100字，建议阅读6分钟
对程序员而言，对数学思维的强调永远不会过分，要写出好代码，不能惧怕数学。

图灵奖得主、分布式系统先驱、LaTeX之父Leslie Lamport认为，对于程序员而言，对数学思维的强调永远不会过分，要写出好代码，不能惧怕数学。

Leslie Lamport可能不是一个家喻户晓的名字，但一提到和他有关的研究，相信你一定不陌生。

排版程序LaTeX和分布式系统。前者发过论文的都懂，后者则使谷歌和亚马逊的云基础设施成为可能。

2013年，Lamport因其在分布式系统方面的工作而获得图灵奖（A.M. Turing Award）。

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

有了分布式系统，互联网搜索、云计算和人工智能都可以协调强大的计算机器集群一起工作。

不过，这类系统也存在一些不可避免的问题。

Lamport曾经说过：「在分布式系统中，你甚至不知道存在的计算机故障，会使你自己的计算机无法使用。」

其中最大的问题来源是 「并发系统」，多个计算操作会发生在重叠的时间片段上，导致了模糊不清的情况。哪台计算机的时钟是正确的？

在1978年的一篇开创性的论文中，Lamport引入了「因果关系」的概念来解决这个问题，使用的是狭义相对论的一个观点。

两个观察者可能对事件的顺序有异议，但如果一个事件导致了另一个事件，这就消除了模糊性。而发送或接收一个信息可以在多个过程中建立因果关系。逻辑时钟——现在也称为「Lamport时钟」提供了一种推理并发系统的标准方法。

有了这个工具，计算机科学家接下来想知道，他们如何能够系统地扩大这些连接的计算机集群的规模，同时不增加错误的数量。Lamport提出了一个优雅的解决方案。

Paxos，这是一种 「共识算法」，允许多台计算机执行复杂的任务。没有Paxos和它的算法系列，现代分布式计算就不可能存在。

20世纪80年代初，Lamport还创建了LaTeX，这是一个文档准备系统，为复杂公式的排版和科学文件的格式提供了复杂的方法。

现在，LaTeX不仅在数学和计算机科学领域，而且在大多数科学领域都已成为论文格式的主流标准。

自20世纪90年代以来，Lamport的工作重点是 "形式验证"，即使用数学证明来验证软件和硬件系统的正确性。值得注意的是，他创造了一种名为TLA+（行动的时间逻辑）的 "规范语言"。

大师专访：用数学的思考写算法

最近，QuantaMagazine与Lamport谈了他在分布式系统方面的工作，计算机科学教育的问题，以及使用TLA+如何帮助程序员建立更好的系统。

以下是访谈内容简编。

让我们从Paxos开始，因为它是如此有影响力的算法。是什么让你一开始就开始研究这个问题？

人们正在用一些代码建立一个系统，我有一种预感，他们的代码试图完成的事情是不可能的。所以我决定尝试证明这一点，并想出了一种算法，而这些人本应在他们的系统中使用我这种算法。

他们原来的算法有什么问题？

嗯，他们其实没有算法，只有一堆代码。很少有程序员从算法上思考问题。当你试图编写一个并发系统时，如果你只是写代码，而没有算法，你的程序里就一定全是错误。

介绍Paxos的那篇论文起初并没有被广泛阅读。为什么？

让人们无法阅读论文的原因是，我喜欢通过讲故事来解释事情，而且我为角色编造了一些伪希腊字母的名字。

例如，在论文中，有一个名叫Γωυδα的奶酪检查员。我是作为数学家长大的，整天和希腊字母打交道，不知道非数学家会不会被这些字母完全吓坏了。 

显然，这对很多读者而言是个问题，所以读那篇文章的人少了不少。

一开始效果并不理想。虽然从长远来看，它确实如此，因为人们称这个共识算法系列为Paxos，而不是 「viewstamped replication」，这是计算机科学家Barbara Liskov对该算法的另一个称谓。

在从事了这么多年的分布式系统工作后，是什么让你又开始搞TLA+的？

在20世纪70年代，当人们对程序进行推理时，实际上是在证明程序本身的属性，再以编程语言的方式陈述出来。后来人们意识到，其实应该首先说明程序应该完成什么任务，即程序的行为。

到了80年代初，我意识到为并发系统编写这些高级规范的一个实用方法，就是把它们写成抽象的算法。有了TLA+，我就能以一种完全严谨的方式来表达。一切都变得简单了。

这就意味着基本上不能用编程语言来写算法。如果你真的想把事情做对，你需要用数学的术语来写你的算法，你知道这样做一定会成功的。

Lamport认为，在动手写代码之前，要先思考和写作的重要性，这需要在本科计算机科学课程中教授，而现在却没有。

你曾说过，「如果你只是思考，不写代码，你只是认为你在思考而已」。这就是模型检查的作用吗？

模型检查是一种详尽地测试系统的小模型的所有执行情况的方法。它只是显示模型的正确性，而不是算法的正确性。当模型检查测试正确性时，编码只是产生代码。它并不测试任何东西。在有模型检查之前，确定你的算法能正常work的唯一方法是写一个证明。

在实践中，模型检查会检查算法的一个小实例的所有执行情况。如果你很幸运，你可以检查足够大的实例，使你对该算法有足够的信心。

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

Coq的设计是为了做真正的数学，并且能够捕捉数学家所做的推理。例如，Georges Gonthier就是用它来证明四色定理的。一个经过机器检查的数学陈述的证明表明，该陈述几乎肯定是真的。

而TLA+不是为数学家设计的，而是为那些想证明其系统属性的工程师设计的。上世纪90年代，在花了大约15年时间编写并发算法的证明之后，我了解到为了证明一个并发算法的正确性，你需要做什么。

TLA是一种逻辑，它允许所有的完全形式化表述。而TLA+则是基于此的完整语言。

Lamport因在分布式系统方面的工作在2013年获得了A.M. 图灵奖。他提出的Paxos算法，现在已经成为一个行业的通行标准。

像TLA+这样的规范语言在工业界的应用并不广泛，对吗？你认为这是为什么呢？

嗯，我一直在尽力推广这个规范。但基本上，程序员和许多计算机科学家都被数学吓坏了。所以这是一个很艰难的推销过程。

第二，每一个项目都必须在匆忙中完成。有一句老话，"永远没有时间做正确的事。总有时间重做"。因为TLA+涉及前期工作，你在开发过程中增加了一个新的步骤，也会成为一个难点。

这种努力总是值得的吗？

的确，世界各地的程序员所写的大多数代码都不需要非常精确地说明它应该做什么。但是，有些事情是重要的，需要正确的。

当人们建造一个芯片时，他们希望这个芯片能够正常工作。当人们建立一个云基础设施时，他们不希望出现会丢失人们的数据的错误。

对于那种精度很重要的应用，你需要非常严格，需要像TLA+这样的东西，特别是在涉及到并发的情况下，而在这些系统中通常会有并发。

由Lamport在过去几十年中开发的规范语言TLA+，让工程人员可以以精确的数学方式描述程序要实现的目标

程序员花在写代码上的时间比花在思考上的时间多，这是否是一种偏见？

是的，在编写代码之前思考和写作的重要性需要在本科计算机科学课程中教授，而现在却没有。而原因是，教编程的人和教程序验证的人之间没有沟通。

从我所看到的情况来看，错误在于这个鸿沟的两边。教编程的人不知道他们需要知道的验证。教验证的人不了解它应该如何在实践中应用。

在这个鸿沟被填平之前，TLA+是不可能拥有大量用户的。我希望我至少能让教并发编程的人明白，他们需要TLA+。这样也许才会有一些希望。

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

对数学思维的重视不够，是的，远远不够。 

那么，按你的想法，本科计算机课程应该怎样设置？

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

他们只是学了足够的东西来通过考试，然后就把学过的东西忘了。

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

我不从美不美的角度考虑。我可能有其他人的那种感觉，但我会用不同的词来表达。

「美」不是我对算法的评价。但是「简单性」是我非常重视的一点。

最后一个问题，是关于你的另一个项目 LaTeX的。想最后跟你澄清一件事。LaTeX到底怎么读？是LAH-tekh还是LAY-tekh？

想怎么读就怎么读。我建议不要花太多的时间去考虑这个问题。

参考链接：

https://www.quantamagazine.org/computing-expert-says-programmers-need-more-math-20220517/

编辑：于腾凯

校对：林亦霖