热点新闻

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

admin2022-05-25 05:40 206人已围观

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

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

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

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

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

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 参观加州山景城的计算机历史博物馆

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

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

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

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

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

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

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

论文链接：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 + 的确做得很出色。重要的是，不要试图用编程语言来编写算法：如果你真的想把事情做好，你需要用数学的术语来编写你的算法。