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

莱斯利·兰波特可能不是一个家喻户晓的名字，但对于计算机科学家来说，他是一些熟悉的名字背后的贡献者比如Paxos算法，排版程序LaTeX，规范语言TLA+，烘焙算法和拜占庭一般问题等等

莱斯利·兰波特彻底改变了现代计算机相互交流的方式2013年，他因在分布式系统方面的工作获得了图灵奖

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

Lamport曾经说过，分布式系统是一个你甚至不知道存在的计算机发生故障，会让你自己的计算机无法使用的系统。」

有了这个工具，计算机科学家们开始思考如何在不增加bug的情况下，系统地让这些连接的计算机变得更大Lampor提出了一个优雅的解决方案:Paxos，一种允许多台计算机执行复杂任务的一致性算法没有Paxos及其算法家族，现代计算就不可能存在Paxos算法现在已经成为行业标准

Lamport的另一个贡献是，他在20世纪80年代初构建了文档准备系统LaTeX，该系统提供了复杂的公式和科学的文档格式LaTeX不仅在数学和计算机科学领域，而且在大多数科学领域都成为了纸张格式的标准

此外，Lamport开发的规范语言TLA+使工程师能够以精确和数学的方式描述程序的目标自20世纪90年代以来，Lamport的工作一直专注于形式验证，即使用数学证明来验证软件和硬件系统的正确性他的突出贡献是创造了一种叫做TLA+的规范语言软件规格说明就像一个程序的蓝图或公式，它描述了软件应该如何在高层次上运行这并不总是必要的，因为编写一个简单的程序就像煮鸡蛋一样但如果是更复杂，风险更大的任务，就需要更高的精度写这样一个程序，就相当于准备了一场九道菜的盛宴你需要准备每一道菜的每一种成分，以精确的方式组合它们，然后按照正确的顺序提供给每位客人这需要准确的食谱和说明，而且要用清晰简洁的语言写出来可是，用英语散文写作可能会导致误解TLA+使用精确的数学语言来防止错误和避免设计缺陷

以你的菜谱或规格为输入，一个名为Model Checker的程序会检查菜谱是否合理，是否按预期工作，从而按照厨师的要求做出一道菜在Lamport为程序员编写适当的规范之前，程序员经常会随意拼凑一个系统，这一度让他感到遗憾毕竟，一个厨师不可能在不知道他的食谱是否正确的情况下为宴会准备食物

这些成就不是偶然的这位81岁的计算机科学家对人们如何使用和思考软件有着不同寻常的洞察力

最近，Quanta杂志对Lamport进行了专访，讨论他在分布式系统方面的工作在采访中，Lamport谈到了他创造的TLA+语言如何帮助程序员构建更好的系统，还谈到了当前计算机科学教育中存在的问题，强调了数学思维在计算机科学中的重要性

《艾科技评论》在不改变初衷的基础上整理了这篇采访，为读者奉上晚餐。

兰波特参观位于加州山景城的计算机历史博物馆

Quanta:先说Paxos，因为它是一个很有影响力的算法你能告诉我是什么驱使你开始这项工作吗

兰波特:当时人们用一些代码来构建一个系统我有一种预感，他们的代码想要达到的目标是不可能的因此，我决定尝试证明它，并提出一种人们应该在他们的系统中使用的算法

广达:他们原来的算法有什么问题。

Lamport:他们没有算法，只有一堆代码很少有程序员用算法来思考问题在尝试写并发系统的时候，如果只写代码不写算法，那么你的程序必然充满bug

Quanta:介绍Paxos的论文一开始并没有被广泛阅读为什么会这样

Lamport:可能原因是我喜欢用故事来解释事情，我用希腊字母来给人物命名比如论文里有一个奶酪检查员叫γ ω и δ α作为数学家，希腊字母在这里随处可见只是没想到那些不是数学家的人会被这些字母吓到这就导致了本该看到却没看到的论文

所以一开始Paxos的应用效果并不是很好，但是从长远来看确实达到了目的，因为人们把这一系列的共识算法叫做Paxos，而不是viewstamped replication。

广达:在分布式系统领域研究了这么多年，是什么让你开始了创建TLA+的工作。

Lamport:在20世纪70年代，当人们对程序进行推理时，他们试图证明程序本身的属性，这些属性是用编程语言表达的后来人们意识到，他们真的应该先解释程序应该完成什么——也就是程序的行为

在20世纪80年代早期，我意识到为并发系统编写这些高级规范的实际方法是将它们编写为抽象算法有了TLA+，我可以用足够严谨的方式用数学来表达它们后来事实证明，that做得非常出色重要的是不要试图用编程语言写算法:如果你真的想把事情做好，你需要用数学术语写你的算法

广达:你曾经说过:如果你只思考不写作，你只会思考你在思考的东西这是模型检查的目的吗

Lamport:模型检查是全面检查系统小模型所有执行情况的方法只说明模型的正确性，不说明算法的正确性当用模型检查来验证正确性时，编码只是生成代码，并不测试任何东西在模型检查之前，保证算法有效性的唯一方法就是写一个证明

在实践中，模型检查将检查算法的一个小实例的所有执行运气好的话，可以查足够多的例子，让你对算法有足够的信心但对于任何规模的系统和算法的使用，证明可以验证其正确性

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

兰波特:COQ的目的是解决真正的数学问题它可以捕捉数学家做出的推理比如乔治·冈蒂尔用它证明了四色定理一个数学命题的证明经过机器验证后，几乎可以确定该命题为真

TLA+不是为数学家设计的，而是为那些想要证明他们系统特性的工程师设计的90年代，写了大概15年并发算法的证明之后，我才知道要证明并发算法的正确性需要做什么TLA是一种可以让证明过程完全形式化的逻辑，TLA+也是一套完整的基于TL逻辑的语言

Quanta:像TLA+这样的规范语言在工业界没有被广泛使用，是吗你认为这是为什么

兰波特:我尽力了但基本上，程序员和许多计算机科学家都被数学吓坏了因此，它的销售非常困难

此外，每个项目都必须匆忙完成有一句老话，永远没有足够的时间来完美地做一件事，但总有时间重新开始TLA+没有被广泛使用，因为它涉及到前期工作，并在开发过程中增加了新的步骤

广达:前期的工作总是值得的吗。

Lamport:的确，全世界程序员写的大多数代码都不需要非常精确的语句来解释它应该做什么但是有些事情很重要，需要保证正确

例如，当人们制造芯片时，他们希望芯片能够正常工作当人们构建云基础设施时，他们不希望出现会丢失人们数据的错误对于那些要求精度的应用，你需要非常严格你需要类似于TLA+的东西，尤其是当涉及到通常存在于这些系统中的并发性时

Quanta:程序员倾向于花更多的时间写代码而不是思考吗。

Lamport:是的，在编写代码之前思考和写作的重要性需要在本科计算机科学课程中教授，但事实并非如此原因是教编程的和教程序验证的没有交流

在我看来，这个分歧双方都有问题教编程的不懂需要知道的验证，教验证的不懂在实践中应该如何应用和使用

在这个鸿沟被弥合之前，TLA+不会获得大量用户希望我至少能让教并发编程的人明白，他们需要TLA+那样的话，that可能会被更多人使用

广达:我感觉你对这几年的计算机科学教育不太满意是因为我们对数学不够重视吗

兰波特:是的，在数学思维方面。

广达:那么，你将如何构建本科课程。

量子:数学家常说在数学中看到美你是从算法领域起步的，那么你看到算法的美了吗

兰波特:我不从审美的角度考虑这个问题我可能和别人的感受一样，只是用不同的语言表达而已关于算法，我不考虑美观，但是简单是我非常看重的东西

参考链接: