莱斯利 · 兰波特彻底改变了计算机之间的交流方式。如今，他正致力于研究工程师如何与自己的机器交流。
计算机科学家莱斯利·兰波特的成果使得现代计算机能够有效地相互协调。从那以来，他将注意力转向了提高编程本身的效率
莱斯利 · 兰波特（Leslie Lamport）也许不是一个家喻户晓的名字，但对于计算机科学家而言，他是以下成果的幕后功臣：排版程序LaTeX，以及使谷歌和亚马逊的云基础设施成为可能的研究。他还引领人们对一些问题给予了更多关注，给这些问题起了具有特点的名字，比如“面包店算法”和“拜占庭将军问题”。这绝非偶然。这位81岁的计算机科学家对于人们如何使用和看待软件有着异乎寻常的缜密考量。
2013年，他因在分布式系统方面的工作获得了图灵奖，它被认为是计算机领域的诺贝尔奖。分布式系统是指不同网络上的多个组件协同工作以实现共同目标的系统。互联网搜索、云计算和人工智能都涉及协调强大的计算机集群共同工作。当然，这种协作会带来更多的问题。
兰波特曾经说过：“在分布式系统中，若有一台你甚至不知其存在的计算机出现故障，就可能导致你自己的计算机无法使用。”
其中最大的问题来源是“并发系统”，该系统中，多个计算操作会发生在重叠的时间片段上，致使模糊发生：哪台计算机的时钟才是正确的？在1978年一篇开创性的论文中，兰波特利用狭义相对论中的某个观点，引入了“因果关系”的概念来解决这个问题。两个观察者可能对事件的顺序存在分歧，但是如果一个事件导致另一个事件，那么模糊性就得到了消除。发送或接收消息可以在多个进程之间建立因果关系。逻辑时钟——现在也称为兰波特时钟——提供了一种推断并发系统的标准方法。
有了这个工具，计算机科学家们接下来想知道他们如何能够系统地扩大这些连接的计算机的规模，同时不增加错误数量。兰波特提出了一个优雅的解决方案：Paxos，一种允许多台计算机执行复杂任务的“共识算法”。如果没有Paxos及其算法家族，现代计算就不可能存在。
在20世纪80年代早期，兰波特在开发这一领域时还创建了LaTeX，这是一个文档准备系统，它为复杂公式的排版和科学文档的格式编排提供了精密巧妙的方式。LaTeX不仅在数学和计算机科学领域，而且在大多数科学领域都已成为论文格式编排的标准。
兰波特参观加利福尼亚州山景城的计算机历史博物馆
自20世纪90年代以来，兰波特的工作主要集中在“形式验证”上，即利用数学证明来验证软件和硬件系统的正确性。值得注意的是，他创建了一种名为行为时序逻辑（TLA+）的“规范语言”。软件规范就像是程序的蓝图或配方，它描述了软件在高层次上应该如何运行。这并非总是必需的，因为编写一个简单的程序就和煮鸡蛋一样轻松。但是，一个更加复杂、风险更高的任务——相当于一场九道菜的宴席——则要求更高的精确度。你需要准备好每道菜的每个组成部分，将它们以一种精确的方式组合起来，随后按照正确的顺序提供给每位客人。这就需要用明确简洁的语言写出准确的食谱和说明，但用英语写出的描述可能会留下误解的空间。TLA+采用精确的数学语言来防止错误、避免设计缺陷。
一个叫做“模型检查器”的程序会把你的“食谱”——也就是规范——当作输入，以检查食谱是否有意义、是否按照预期的方式工作，从而按照厨师的要求生产出一道菜。兰波特抱怨道，程序员时常先拼凑出一个系统，然后才编写正确的规范，然而厨师若不事先知道他们的食谱可行，是绝不会为宴会提供食物的。
《量子杂志》与兰波特讨论了他在分布式系统方面的工作、计算机科学教育中的问题，以及使用TLA+如何能帮助程序员构建更好的系统。为了清晰起见，下述访谈内容经过了整理简编。
让我们从Paxos开始聊吧，因为它是一个影响力如此之大的算法。你最初是出于什么理由着手开发它的？
人们用一些代码建立了一个系统，而我有预感，他们的代码想要完成的事情是不可能做到的。所以我决定尝试证明这一点，并且想出了一种算法——人们理应在他们的系统中使用这种算法。
他们原来的算法有什么问题？
这个嘛，他们原有的其实并非算法，而只是一堆代码。很少有程序员从算法层面思考问题。在尝试编写并发系统时，如果只是编写代码而不使用算法，那么你的程序里必然全是错误。
介绍Paxos的那篇论文起初并没有得到广泛的阅读。为什么会这样？
令人们无法阅读这篇论文的原因是我喜欢用故事来解释事物，而且我还为角色起了一些伪希腊字母的名字。例如，在论文中有一个奶酪检查员名叫Γωδα。作为一个数学家，我整天和希腊字母打交道，也就没有意识到非数学家会被这些字母吓到。显然，它们对读者来说是个问题，因此读这篇论文的人比预计的要少了许多。
所以，起初它的接受度并不高。尽管从长远来看，它还是得到了广泛的认可，因为人们把这个共识算法家族称为“Paxos”，而非“视图戳记复制”（viewstamped replication），后者是计算机科学家芭芭拉 · 利斯科夫（Barbara Liskov）给同一算法起的另一个名字。
在从事了这么多年的分布式系统工作之后，又是什么让你开始研究TLA+的？
在20世纪70年代，当人们还在对程序进行推理的时候，他们在做的是证明程序本身的属性，并将这些属性以编程语言的方式表述出来。随后人们意识到，他们真正应该表述的是程序应该首先完成的任务，也就是程序的行为。
在20世纪80年代早期，我意识到为并发系统编写这些高级规范的一种实用方法是将它们作为抽象算法来编写。通过TLA+，我能够以一种完全严谨的方式在数学层面表达它们。于是一切都变得顺利了。基本而言，这其中所涉及的并非试图用编程语言来编写算法：如果你真的想把事情做对，你需要用数学的方式来编写算法。
你曾经说过，如果你光思考却不写，那你就只是自认为在思考罢了。这就是模型检查的作用吗？
模型检查是对系统的小模型的所有执行情况进行详尽测试的一种方法。它只显示模型的正确性，而非算法的正确性。当模型检查测试正确性时，编码只生成代码。它并不测试任何东西。在模型检查出现之前，确保算法有效的唯一方法是编写一个证明。
在实践中，模型检查会检查算法的一个小实例的所有执行情况。如果你足够幸运，你可以检查足够大的实例，这会让你对算法产生足够的信心。但这一证明可以确证它对于任何规模的系统和算法的任何应用都是正确的。
听起来，模型检查与另一种程序验证方法有关：使用Coq等工具进行交互式定理证明。它们有什么不同？
Coq旨在进行真正的数学运算，并能够捕捉数学家所做的推理。例如，乔治 · 龚提尔（Georges Gonthier）正是用它证明了四色定理。一个经过了机器检查的数学陈述的证明表明，该陈述几乎肯定为真。
TLA+不是为数学家设计的，而是为那些想要证明其系统属性的工程师设计的。20世纪90年代，在花费了大约15年的时间编写并发算法的证明之后，我了解到了需要做哪些事才能证明并发算法的正确性。TLA是一种允许完全形式化的逻辑。TLA+则是基于此的完整语言。
兰波特在过去几十年里开发的规范语言TLA+允许工程师以精确的数学方式描述程序的目标
兰波特认为，在编程前先行思考和写作极为重要，这一点需要在本科计算机科学课程中进行教授，但实际并未如此
兰波特因其在计算机协作（该领域被称为分布式系统）方面的成果获得了2013年的图灵奖。他的Paxos算法现已成为行业标准
像TLA+这样的规范语言并没有在行业中得到广泛的应用，对吧？你认为这是为什么呢？
这个嘛，我尽力而为了。但基本上，程序员和许多计算机科学家（甚至是绝大多数计算机科学家）都对数学心怀恐惧。所以这是一个很艰难的推广过程。
其次，每个项目都必须在匆忙中完成。有句老话说：“永远没有时间去把事情做对。但总有时间把事情再做一遍。”由于TLA+涉及一些前期工作，这意味着你在开发过程中添加了一个新步骤，这也让它的推广变得很难。
这种前期努力是否总是值得？
的确，世界各地的程序员所编写的大多数代码并不需要事先非常精确地说明它应该做到什么。但有些的确重要，它们需要是正确无误的。
当人们制造芯片的时候，他们希望芯片能正常工作。当人们构建云基础设施时，他们不希望出现会丢失人们数据的错误。对于那种精度非常重要的应用程序，你需要非常严格，需要类似TLA+这样的东西，特别是在涉及并发的情况下，而这些系统中通常都会涉及并发。
程序员是否倾向于把更多的时间花在写代码上，而非在思考代码上？
是的，在编程前先行思考和写作极为重要，这一点需要在本科计算机科学课程中进行教授，但实际并未如此。其原因在于，教授程序设计的人和教授程序验证的人之间缺少交流。
在我看来，这一分歧的双方都有错。教编程的人不了解验证，但他们理应了解。教验证的人员则不了解如何在实践中应用验证。
在这一鸿沟弥合之前，TLA+是不会拥有大量用户的。我希望我至少能让教并发编程的人明白他们需要它。这样也许才会有一些希望。
我感觉你对最近的计算机科学教育不太满意。是因为它没有给予数学足够的重视吗？
对数学思维的重视不够，没错。
那么，换做是你的话，会如何构建本科课程呢？
我不是教育工作者，所以我并不清楚怎么教他们数学思维。但我知道人们应该学什么。他们不应该害怕数学。这只是简单的数学，他们可能已经上过一门相关课程，却不知道如何运用它。他们不知道数学有什么好处。他们学到的知识足以通过考试，然后就把学过的东西忘了。
数学家常说他们在数学中看到美。你是从这个领域起步的，那么你看到算法之美了吗？
我不从美学的角度考虑。我可能和其他人有同样的感受，但我会用不同的词语来表述它们。我不会说算法是“美”的。但“简洁”是我非常看重的东西。
最后一个问题，是关于你的另一个具有相当大影响力的项目LaTeX的。我想最后和你这位创造者澄清一件事。它的发音是“LAH-tekh”还是“LAY-tekh”？
哪个都行。我不建议你花太多时间思考这件事。
资料来源 Quanta Magazine
