2013年图灵奖得主 Leslie Lamport 专访：程序员需要更多的数学知识作者｜李梅编辑

文章图片
作者｜李梅
编辑｜陈彩娴LeslieLamport可能并不是一个家喻户晓的名字，但对于计算机科学家们来说，他是一些耳熟能详的「名字」幕后的贡献者。比如Paxos算法、排版程序LaTeX、规格语言TLA+、「面包店算法」和「拜占庭将军问题」等等。
LeslieLamport彻底改变了现代计算机之间的对话方式。 2013年，他被授予图灵奖，以表彰他在分布式系统方面的工作。
在分布式系统中，不同网络上的多个组件协调一致，以实现一个共同的目标。互联网搜索、云计算和人工智能都需要协调众多强大的计算机器协同工作。当然，这种协调也会使我们遇到更多的问题。
Lamport曾经说过：「分布式系统是这样一种系统，在这种系统中，一台你甚至不知晓其存在的计算机出现了故障，就会导致你自己的计算机无法使用。」
最大的问题来源之一是「并发系统」，即在重叠的时间片段内发生多个计算操作，这导致了一种模糊性：哪台计算机的时钟是正确的？在1978年的一篇开创性论文中， Lamport引入了「因果关系」的概念，利用狭义相对论的观点来解决这个问题。两个观察者在事件顺序上可能存在分歧，但如果是一个事件导致另一个事件的发生，那么就能消除模糊性。发送或接收消息可以在多个进程之间建立因果关系。「逻辑时钟」（现在也被称为Lamport时钟），提供了一种标准的方法来对并发系统进行推理。
有了这个工具以后，计算机科学家开始想知道他们如何系统地将这些连接的计算机变得更大，而不增加Bug 。 Lampor提出了一个优雅的解决方案：Paxos ，一种允许多台计算机执行复杂任务的「一致性算法」。没有Paxos及其算法家族，现代计算就不可能存在。 Paxos算法现在已经成为行业标准。
Lamport的另一贡献，是他在上世纪80年代初创建了文档准备系统LaTeX ，提供了复杂公式排版和科学文档格式的复杂方法。不仅在数学和计算机科学领域，而且在大多数科学领域， LaTeX已经成为论文格式的标准。
另外， Lamport所开发的规格语言TLA+使得工程师能够以一种精确的、数学的方式描述程序的目标。自20世纪90年代以来， Lamport的工作就一直专注于「形式验证」（formalverification），即使用数学证明来验证软件和硬件系统的正确性。他的突出贡献便是创建了一种「规格语言」，称为TLA+（TemporalLogicofActions ，行为时序逻辑）。软件规格说明就像一个程序的蓝图或配方，它描述软件应该如何在高层次上运行。这并不总是必要的，因为编写一个简单的程序就像煮一个鸡蛋一样。但若是一项更复杂、风险更高的任务，则需更高的精确度，编写这样一个程序就相当于准备一场九道菜的盛宴。你需要准备每道菜的每个组成部分，以一种精确的方式组合它们，然后按照正确的顺序把它们端给每一位客人。这需要精确的食谱和说明，并以明确简洁的语言来书写，而描写成英语散文，则可能会导致误解。 TLA+使用精确的数学语言来防止错误和避免设计缺陷。
将你的菜谱或规格作为输入，一个叫做模型检查器的程序会检查菜谱是否合理、是否按预期工作，从而按照厨师的要求做出一道菜。在Lamport为程序员编写适当的规格以前，程序员们经常胡乱拼凑一个系统，这曾让他感到惋惜，毕竟厨师在不知道自己的食谱是否正确的情况下，是无法为宴会准备食物的。
这些成就并不是偶然的。这位81岁的计算机科学家对于人们如何使用和思考软件有着不同寻常的见解。