在线客服
企业微信
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科技评论在不改变原意的基础上对该专访进行了编译，以飨读者。
2013年图灵奖得主 Leslie Lamport 专访：程序员需要更多的数学知识
图注：Lamport参观加州山景城的计算机历史博物馆
Quanta：我们先从Paxos谈起，因为它是一个非常有影响力的算法。能否谈谈是什么驱动您开始做这项工作的？
Lamport：当时人们使用一些代码去构建一个系统，我有种预感，他们的代码所试图实现的目标是不可能的。因此，我决定尝试去证明这一点，并提出了一种人们应该在他们的系统中使用的算法。
Quanta：他们原有的算法存在什么问题？
Lamport：他们并没有算法，而是只有一堆代码。很少有程序员用算法来思考问题。在尝试编写并发系统时，如果只编写代码而没有算法，那么你的程序必然会到处都是bug。
