EN

2013 年图灵奖得主 Leslie Lamport 专访:程序员需求更多的数学

发布日期:2022-05-25 12:53:27 来源:Kok体育网页

  Leslie Lamport 或许并不是一个众所周知的姓名,但关于核算机科学家们来说,他是一些耳熟能详的「姓名」暗地的奉献者。比方 Paxos 算法、排版程序 LaTeX、标准言语 TLA+、「面包店算法」和「拜占庭将军问题」等等。

  Leslie Lamport 彻底改变了现代核算机之间的对线 年,他被颁发图灵奖,以赞誉他在分布式体系方面的作业。

  在分布式体系中,不同网络上的多个组件和谐一致,以完结一个一起的方针。互联网查找、云核算和人工智能都需求和谐很多强壮的核算机器协同作业。当然,这种和谐也会使咱们遇到更多的问题。

  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+ 言语怎么协助程序员构建更好的体系,还谈及了其时核算机科学教育中存在的问题,强调了数学思想在核算机科学中的重要性。

  Quanta:咱们先从 Paxos 谈起,由于它是一个十分有影响力的算法。能否谈谈是什么驱动您开端做这项作业的?

  Lamport:其时人们运用一些代码去构建一个体系,我有种预见,他们的代码所企图完结的方针是不或许的。因而,我决议测验去证明这一点,并提出了一种人们应该在他们的体系中运用的算法。

  Lamport:他们并没有算法,而是只要一堆代码。很少有程序员用算法来考虑问题。在测验编写并发体系时,假如只编写代码而没有算法,那么你的程序必然会处处都是 bug。

  Lamport:原因或许是我喜爱用故事来解说作业,并且我用希腊字母来为人物命名。例如,在论文中,有一位奶酪查看员名叫 ΓωИΔα。身为一名数学家,在这里随处可见希腊字母,我仅仅没有意识到那些不是数学家的人会被这些字母给吓到。这导致了这篇本来应该被看见的论文而没有被看见。

  所以在一开端 Paxos 的运用作用并不太好,但从久远来看它确实完结了它的方针,由于人们称这一系列的一致算法为 Paxos,而不是「viewstamped replication」(这是核算机科学家、图灵奖得主 Barbara Liskov 对一致算法的另一个命名)。

  Lamport:在 20 世纪 70 时代,当人们对程序进行推理时,他们企图证明程序自身的特点,这些特点是用编程言语表述的。后来人们意识到,他们确实应该阐明程序首先要完结什么——即程序的行为。

  在 20 世纪 80 时代初,我意识到,为并发体系编写这些更高等级标准的有用办法,是将它们编写为笼统的算法。有了 TLA+,我就可以以一种满足谨慎的办法用数学去表达它们。后来证明,TLA+ 确实做得很超卓。重要的是,不要企图用编程言语来编写算法:假如你真的想把作业做好,你需求用数学的术语来编写你的算法。

  Quanta:您曾说过,「假如你只考虑而不写作,你就只会考虑你在考虑的东西。」这便是模型检测(model checking)的意图吗?

  Lamport:模型检测是一种全面检测体系小模型的一切履行情况的办法。它只显示模型的正确性,而不是算法的正确性。当模型检测去验证正确性时,编码只会生成代码,它不测验任何东西。在进行模型检测之前,确保算法有用的仅有办法是写证明(proof)。

  在详细实践中,模型检测会查看算法的一个小实例的一切履行情况。假如走运的话,您可以查看满足多的实例,然后使你对算法有满足的决心。但关于任何规划的体系和算法的运用,证明都可以验证其正确性。

  Quanta:听起来,模型检测与另一种程序验证办法有关:运用 Coq 等东西进行交互式定理证明。它们有何不同?

  Lamport:Coq 的意图是处理真实的数学问题,它可以捕捉数学家所做的推理。例如, Georges Gonthier 用它来证明了四色定理(four-color theorem)。一个数学出题的证明通过机器验证后,简直可以必定该出题为真。

  TLA+ 不是为数学家规划的,而是为期望证明其体系特性的工程师规划的。20 世纪 90 时代,在花了大约 15 年的时刻编写并发算法的证明之后,我了解到为了证明并发算法的正确性需求做什么。TLA 是可以一种让证明进程具有彻底的办法化的逻辑,并且 TLA+ 也是根据 TL 逻辑的一套完好言语。

  Quanta:像 TLA+ 这样的标准言语在工业中运用得不是很广泛,是吗?您以为这是为什么?

  Lamport:我正在尽我所能。但基本上,程序员和许多(假如不是大多数的话)核算机科学家都被数学给吓坏了。所以它的「销路」很困难。

  别的,每个项目都必须急匆匆地赶完。有句老话,「永久没有满足的时刻把一件事做到完美,但总是有时刻去从头来过。」由于 TLA+ 涉及到前期作业,在开发进程中又会增加新过程,所以这也导致了它没有被广泛运用。

  Lamport:确实,世界各地的程序员编写的大多数代码都不需求十分准确的句子来阐明它应该做什么。但有些作业很重要,需求确保正确。

  例如,当人们制作芯片时,他们期望芯片能正常作业。当人们构建云基础设施时,他们不期望呈现会丢掉人们数据的 bug。关于那些要求精度的运用程序,你需求十分严厉。并且你需求类似于 TLA+ 的东西,尤其是当涉及到一般存在于这些体系中的并发时。

  Lamport:是的,在编写代码之前进行考虑和写作的重要性,需求在本科的核算机科学课程中教授,但现实并非如此。原因是教编程的人和教程序验证的人之间没有沟通。

  就我所见,这一不合的两头都存在问题。教编程的人不了解他们需求知道的验证,而教授验证的人不理解它应该怎么运用和在实践中运用。

  在弥合这一距离之前,TLA+ 是不会收成很多用户的。我期望我至少能让教授并发编程的人理解他们需求 TLA+。那样的话,TLA+ 或许还有期望被更多人运用。

  Lamport:我不是一个教育家,所以我不知道怎么教他们。但我知道人们应该学到什么。他们不应该惧怕数学。他们或许学过一门简略的数学,但不知道怎么运用它。他们不知道这有什么优点。他们学了满足多的常识,通过了考试,然后就抛之脑后。

  Quanta:数学家常说他们在数学中看到了美。你是从算法范畴起步的,那么您看到算法之美了吗?

  Lamport:我并不从美学的视点来考虑。我或许和其他人有相同的感觉,但我仅仅用不同的言语来表达。关于算法,我考虑的不是美,简略是我十分垂青的东西。

线