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

最近， QuantaMagazine对Lamport进行了一次专访，讨论了他在分布式系统方面的工作。在采访中， Lamport谈论了他所创建的TLA+语言如何帮助程序员构建更好的系统，还谈及了当前计算机科学教育中存在的问题，强调了数学思维在计算机科学中的重要性。
AI科技评论在不改变原意的基础上对该专访进行了编译，以飨读者。

文章图片
图注：Lamport参观加州山景城的计算机历史博物馆
Quanta：我们先从Paxos谈起，因为它是一个非常有影响力的算法。能否谈谈是什么驱动您开始做这项工作的？
Lamport：当时人们使用一些代码去构建一个系统，我有种预感，他们的代码所试图实现的目标是不可能的。因此，我决定尝试去证明这一点，并提出了一种人们应该在他们的系统中使用的算法。
Quanta：他们原有的算法存在什么问题？
Lamport：他们并没有算法，而是只有一堆代码。很少有程序员用算法来思考问题。在尝试编写并发系统时，如果只编写代码而没有算法，那么你的程序必然会到处都是bug 。
Quanta：介绍Paxos的那篇论文（“ThePart-TimeParliament”）起初并没有被广为阅读。为什么会这样？

文章图片
论文链接：https://dl.acm.org/doi/pdf/10.1145/279227.279229
Lamport：原因可能是我喜欢用故事来解释事情，而且我用希腊字母来为人物命名。例如，在论文中，有一位奶酪检查员名叫ΓωИΔα 。身为一名数学家，在这里随处可见希腊字母，我只是没有意识到那些不是数学家的人会被这些字母给吓到。这导致了这篇原本应该被看见的论文而没有被看见。
所以在一开始Paxos的应用效果并不太好，但从长远来看它的确实现了它的目标，因为人们称这一系列的共识算法为Paxos ，而不是「viewstampedreplication」（这是计算机科学家、图灵奖得主BarbaraLiskov对共识算法的另一个命名）。
Quanta：在分布式系统领域研究了这么多年之后，是什么让您开始了创建TLA+的工作？
Lamport：在20世纪70年代，当人们对程序进行推理时，他们试图证明程序本身的属性，这些属性是用编程语言表述的。后来人们意识到，他们确实应该说明程序首先要完成什么——即程序的行为。
在20世纪80年代初，我意识到，为并发系统编写这些更高级别规格的实用方法，是将它们编写为抽象的算法。有了TLA+ ，我就能够以一种足够严谨的方式用数学去表达它们。后来证明， TLA+的确做得很出色。重要的是，不要试图用编程语言来编写算法：如果你真的想把事情做好，你需要用数学的术语来编写你的算法。
Quanta：您曾说过，「如果你只思考而不写作，你就只会思考你在思考的东西。」这就是模型检测（modelchecking）的目的吗？
Lamport：模型检测是一种全面检测系统小模型的所有执行情况的方法。它只显示模型的正确性，而不是算法的正确性。当模型检测去验证正确性时，编码只会生成代码，它不测试任何东西。在进行模型检测之前，确保算法有效的唯一方法是写证明（proof）。
在具体实践中，模型检测会检查算法的一个小实例的所有执行情况。如果幸运的话，您可以检查足够多的实例，从而使你对算法有足够的信心。但对于任何规模的系统和算法的使用，证明都可以验证其正确性。
Quanta：听起来，模型检测与另一种程序验证方法有关：使用Coq等工具进行交互式定理证明。它们有何不同？