Q&A:如何编辑数学完美的软件

编辑 | 白菜叶Leslie Lamport 能够不是一个家喻户晓的名字,但他是其中一些计算机科学家的幕后推手:排版次序 LaTeX 以及使 Google 和 Amazon 的云基础设施成为能够的工作

编辑 | 白菜叶

Leslie Lamport 能够不是一个家喻户晓的名字,但他是其中一些计算机科学家的幕后推手:排版次序 LaTeX 以及使 Google 和 Amazon 的云基础设施成为能够的工作。

他还对一些成绩给予了更多关注,给它们起了独特的名字,比如面包店算法和拜占庭将军成绩。这绝非偶然。这位 81 岁的计算机科学家对人们如何应用和考虑软件有着不同寻常的深思熟虑。

图片

2013 年,他赢得了被认为是计算领域诺贝尔奖的图灵奖,表彰了他在分布式体系方面的工作,其中包括不同网络上的多个组件相互协调以实现共同目标。互联网搜索、云计算和人工智能都涉及编排强大的计算机军团协同工作。当然,这种协调会给你带来更多的成绩。

「分布式体系是一个你甚至不晓得存在的计算机的故障,能够导致你自己的计算机无法应用的体系。」Lamport 曾经说过。

成绩的最大来源之一是「并发体系」,其中多个计算操作发生在重叠的时间片中,导致模棱两可:哪台计算机的时钟是准确的?在 1978 年的一篇开创性论文中,Lamport 利用狭义相对论的见解引入了「因果关系」的概念来解决这个成绩。两个观察者能够在事件的顺序上存在分歧,但如果一个事件导致另一个事件,这就消除了歧义。并且发送或接收消息可以在多个进程之间建立因果关系。逻辑时钟——现在也称为 Lamport 时钟——提供了一种推理并发体系的标准方法。

图片

论文链接:https://dl.acm.org/doi/10.1145/359545.359563

有了这个工具,计算机科学家接下来想晓得他们如何体系地使这些连接的计算机变得更大,而不会增加错误。Lamport 提出了一个优雅的解决方案:Paxos,一种允许多台计算机执行复杂任务的「共识算法」。如果没有 Paxos 及其算法家族,就不能够存在现代计算。

在 1980 年代初期,随着他开发该领域,Lamport 还创建了 LaTeX,这是一个文档准备体系,它提供了复杂的方法来排版复杂的公式和格式化科学文档。LaTeX 已成为格式化论文的标准,不仅在数学和计算机科学领域,而且在大多数科学领域也是如此。

Lamport 自 1990 年代以来的工作重点是「形式考证」,即应用数学说明来考证软件和硬件体系的准确性。值得注意的是,他创建了一种名为 TLA+(用于 Temporal Logic of Actions)的「范例说话」。软件范例就像次序的蓝图或配方;它描述了软件在高层次上的行为方式。这并不总是必要的,因为编辑一个简单的次序类似于煮鸡蛋。但更复杂、风险更高的任务——相当于九道菜宴会的编码——需求更高的精度。

你需求准备好每道菜的每个成分,以精确的方式将它们组合在一起,然后以准确的顺序将它们提供给每位客人。这需求准确的食谱和说明,以明确和简洁的说话编辑,但用英语散文编辑的描述能够会留下误解的空间。TLA+ 采用精确的数学说话来防止错误并避免设计缺陷。

应用你的食谱或规格作为输入,称为模型查验器的次序将查验食谱是否有意义并按预期工作,以厨师想要的方式制作菜肴。Lamport 感叹次序员如何在编辑适当的范例之前经常拼凑一个体系,而厨师永远不会在不晓得他们的食谱是否有效的情况下准备宴会。

媒体与 Lamport 讨论了他在分布式体系方面的工作、计算机科学教育出了什么成绩,以及应用 TLA+ 如何帮助次序员建立更好的体系。

Q:让我们从 Paxos 开始,因为它是如此有影响力的算法。是什么让你首先开始研究它?

A:人们正在用一些代码建立一个体系,我有预感,他们的代码试图完成的事情是不能够的。因此,我决定尝试说明这一点,而是提出了一种人们应当在他们的体系中应用的算法。

Q:他们原来的算法有什么成绩?

A:好吧,他们没有算法,只有一堆代码。很少有次序员从算法的角度考虑。在尝试编辑并发体系时,如果你只是编辑代码而不应用算法,那么你的次序就不会充满错误。

Q:介绍 Paxos 的论文起初并没有被广泛阅读。那是为什么?

图片

论文链接:https://dl.acm.org/doi/10.1145/279227.279229

使人们无法阅读这篇论文的原因是我喜欢用故事来解释事物,并且我用某种伪希腊字母为角色命名。例如,论文中提到过一位名叫 Γωυδα 的奶酪查验员。作为一名数学家长大,希腊字母到处都是,我只是不晓得非数学家完全被这些字母吓坏了。显然,读者无法处理它,这导致该论文没有按应有的方式阅读。

所以一开始效果并不好。尽管从长远来看确实如此,因为人们将这一系列共识算法称为 Paxos,而不是「viewstamped replication」,后者是 [计算机科学家] Barbara Liskov 对同一算法的另一个名称。

Q:从事分布式体系多年,是什么让你进入 TLA+?

A:在 1970 年代,当人们对次序进行推理时,他们正在说明次序本身以编程说话的形式表述的属性。然后人们意识到他们真的应当先说明次序应当首先完成什么——次序的行为。

在 1980 年代初期,我意识到为并发体系编辑这些高级范例的一种实用方法是将它们编辑为抽象算法。应用 TLA+,我能够以完全严谨的方式在数学上表达它们。一切都点击了。这涉及的基本上不是试图用编程说话编辑算法:如果你真的想把事情做好,你需求用数学的方式来编辑你的算法。

Q:你说过,「如果你在考虑而不写作,你只会认为你在考虑。」 这就是模型查验的用武之地吗?

A:模型查验是一种详尽地测试体系小模型的所有执行的方法。它只是显示模型的准确性,而不是算法的准确性。在模型查验测试准确性时,编码只是产生代码。它不测试任何东西。在进行模型查验之前,确保你的算法有效的唯一方法是编辑说明。

在实践中,模型查验查验算法的一个小实例的所有执行。如果幸运的话,你可以查验足够大的实例,从而使你对算法有足够的信心。但是这个说明可以说明它对于任何规模的体系和算法的任何应用都是准确的。

Q:听起来模型查验与另一种次序考证方法有关:应用 Coq 等工具进行交互式定理说明。它们有何不同?

A:Coq 旨在进行真正的数学运算,并能够捕捉数学家所做的推理。例如,Georges Gonthier 就是用它来说明四色定理。数学陈述的机器查验说明表明该陈述几乎肯定是准确的。

TLA+ 不是为数学家设计的,而是为想要说明其体系属性的工程师设计的。在 1990 年代,在花了大约 15 年时间编辑并发算法的说明之后,我了解到你需求做什么才能说明并发算法的准确性。TLA 是允许它完全正式的逻辑。TLA+ 是基于此的完整说话。

Q:像 TLA+ 这样的范例说话在工业中并没有被广泛应用,对吧?你认为这是为什么?

A:好吧,我正在做我能做的。但基本上,次序员和许多(如果不是大多数)计算机科学家都被数学吓坏了。所以这是一个艰难的销售。

其次,每个项目都必须匆忙完成。有句老话:「从来没有时间做准确的事。总有时间再做一遍。」 因为 TLA+ 涉及前期工作,所以你在开发过程中添加了一个新步骤,这也是一个很难的推销。

Q:是否总是值得预先付出努力?

A:诚然,全世界次序员编辑的大多数代码都不需求非常精确地说明它应当做什么。但是有些事情很重要,需求准确。

当人们建立芯片时,他们希望该芯片能够正常工作。当人们建立云基础设施时,他们不希望出现会丢失人们数据的错误。对于精度很重要的应用次序,你需求非常严格。你需求像 TLA+ 这样的东西,尤其是在涉及并发的情况下,这些体系中通常会有这种情况。

Q:次序员在编辑代码上花费的时间比他们考虑的时间多吗?

A:是的,在编辑代码之前考虑和写作的重要性需求在本科计算机科学课程中教授,但事实并非如此。原因是教编程的人和教次序考证的人之间没有交流。

从我所看到的情况来看,成绩出在分歧的两边。教编程的人不晓得他们需求晓得的考证。教授考证的人不明白它应当如何在实践中应用和应用。

在弥合这一鸿沟之前,TLA+ 不会找到大量用户。我希望我至少能让教授并发编程的人明白他们需求它。那么也许还有希望。

Q:感觉你现在对计算机科学教育不太满意。是因为它没有对数学给予足够的重视吗?

A:关于数学思维,是的。

Q:那么,你将如何建立本科课程呢?

A:我不是教育工作者,所以我不晓得如何教他们。但我晓得人们应当学到什么。他们不应当害怕数学。这只是简单的数学,他们能够已经上过一门课程,但他们不晓得如何应用它。他们不晓得这有什么好处。他们学到了足够的知识来通过考试,然后他们就忘记了。

Q:数学家经常说他们看到了数学的美。你是从那个领域开始的,所以你看到算法的美吗?

A:我不考虑美学。我能够有其他人的那种感觉,但我只是用不同的词来表达它们。对于算法,我不会说美丽。但简单是我非常看重的东西。

Q:最后一件事,关于你的另一个具有相当大影响的副项目:LaTeX。我想最终与创作者澄清一些事情。它的发音是 LAH-tekh 还是 LAY-tekh?

A:随心所欲。我不建议花太多时间考虑它。

相关报道:https://www.quantamagazine.org/computing-expert-says-programmers-need-more-math-20220517/

原创文章,作者:ScienceAI,如若转载,请注明出处:https://www.iaiol.com/news/27620

(0)
上一篇 2022年5月29日 下午1:03
下一篇 2022年5月30日 下午5:27

相关推荐

发表回复

您的电子邮箱地址不会被公开。 必填项已用*标注