罗伯特·康斯特布尔(Robert Constable)在《逐层修正编程》(corrected by construction programming)一书中写道

路加福音Muehlhauser在你的一些工作中。《比克福德与康斯特布尔》(2008)，您讨论了设计程序的“逐构造修正”和“逐构造安全”方法。你能解释一下这些方法是什么，为什么要使用它们吗?

罗伯特·康斯特布尔：

简短的摘要

编程语言的历史表明，类型是有价值的，因为编译器可以检查程序的类型正确性，并通知程序员他们的代码是否完全符合其类型规范。类型描述了编程任务的需求，在数学和计算中使用的非常丰富的类型系统完全描述了某些技术任务，我们将在下面看到。亚博体育苹果app官方下载类型系统的表达能力越强，规范就越能帮助程序员理解他们的目标亚博体育苹果app官方下载以及实现这些目标的程序。亚博体育苹果app官方下载系统设计者可以用类型精确地指定许多需求和计算任务，并将它们组织成模块(或对象)，这些模块成为分析和构建计算系统的蓝图。

当类型丰富到可以完全指定任务时，我们刚才概述的方法就变成了一个示例正确的施工编程。这种方法已经在数学问题和编程问题上研究了几十年，从60年代末和70年代初就开始了。例如，如果我们想基于算术基本定理(FTA)，每个大于1的自然数都可以被唯一地分解为质数的乘积，我们可以首先将这个任务表示为一个使用类型的编程问题。然后通过编写一个可计算的函数来解决这个问题与适当的类型因素。对于程序员来说，这种类型可能就像FTA定理一样清楚。如下所示。它需要取一个大于1的自然数n作为输入，并返回一组数字(p,e)，其中p是素数，e是它的指数。我们把这个列表写成[(p₁e₁), (p₂e₂),…,(p_ne_n)]并要求n =p₁^e₁X…X p_n^e_np^e意思是' p的e次方，和e_我都是自然数，x是乘法(并且重载为两种类型的笛卡尔积)。另外，全自由贸易区定理要求分解是唯一的。我们稍后将讨论唯一性。对于分解部分，考虑样例因子(24,750)=[(2,1)，(3,2)，(5,3)，(11,1)]。这是正确的，因为24750 = 2 x 9 x 125 x 11，其中5^3.是125。在一个富类型系统中，算术基本定亚博体育苹果app官方下载理的分解部分可以完全描述为一项编程任务结果就是，因素，可以被看作是完成分解的一个建设性证明。类型检查器验证程序是否具有正确的类型。这个项目因素是正确的施工因为已知它具有要解决的问题的类型。

从属类型

这一段有点技术性，可以跳过，也可以作为使用依赖类型的函数式语言进行编码分解的指南。以下是大致的情况分解任务是在Agda, Coq和Nuprl证明助手的编程语亚博体育苹果app官方下载言的类型系统中描述的——稍后再详细介绍。英文的类型规格要求Nat，自然数的类型，0,1,2…并且说:给定一个自然数n大于1,计算对数字的列表,(p, e), p是一个质数,和e是一个自然数,输入值n可以写成一个产品的所有素数p, e每个幂指数(e)搭配它lst列表．象征性地，这可以写成如下N + +是那种(n: Nat n > 1)．我们还定义了类型主要的作为(n: Nat ' (n))为布尔值表达式' (n)我们用哪个函数来编码Nat布尔值。这是FTA分解类型．

(n: n ++) ->(lst:List[Prime x Nat] where n = prod(lst))。

注意，符号x在(' x Nat)表示的类型构造函数命令对的数字。它的元素是有序的对(p, e)正确的类型，p一个主要的和e一个Nat．当然我们需要定义乘积函数，刺激(lst),在一个列表低水位体系域以正确的方式成对。在Agda、Coq和Nuprl等语言中使用函数式编程是很简单的，我们在这些语言中使用了上面使用的函数类型。我们可以把这类编程问题分配给大一的本科生，他们会很容易地解决它，特别是如果我们给他们一个快速的' (n)过程。

另一种编写紧凑解决方案的好方法是使用地图和fold_left通常在列表处理函数库中提供的函数。该解决方案使用了众所周知的方法地图减少范式在函数式编程课程中教授多年，并在工业中广泛使用。使用map和reduce求解是一个很好的练习，因为reduce函数fold_right定义为特定的非常通用的递归程序的列表上的数学归纳法。

历史的角度

从Algol 60到Java和OCaml等主流编程语言的发展表明，类型系统已经变得越来越具有表现力。亚博体育苹果app官方下载例如，现在函数可以被视为对象是标准的，例如，作为输入传递，作为输出产生，并作为显式值创建，就像我们在上面的FTA示例中所做的那样。类型检查和类型推断算法跟上了这一趋势，尽管OCaml还不能检查我们为FTA、Agda、Coq、Nuprl和其他由证明助手支持的编程语言所创建的类型(它们都使用某种形式的)自动推理帮助)。使用非常丰富的类型定义的程序的静态类型检查是一种非常有效的技术，可以精确地指定任务，在编写代码时对代码进行文档化，使代码更容易被其他人读懂(包括几个月后重新访问代码时的自己)，查找错误，以及安全地进行更改。对于函数类型这样的高阶类型，可以精确地定义更多的编程任务，并且可以完全生成代码正确的施工．

到1984年，研亚博体育官网究人员在这种类型检查技术中创造了一个极端点，其中类型系统非常丰富，它们基本上可以完整“正式”地描述任何数学编程任务。亚博体育苹果app官方下载类型还表示对规范所依赖的数据和计算环境的假设。这些极其丰富的类型系统基本上可以表达任何数学问题。亚博体育苹果app官方下载事实上，Coq已经被用来正式证明四色定理以及其他重要的数学定理。证明助手的类型检查通常需要人工干预以及复杂的推理算法。我们所提到的类型系亚博体育苹果app官方下载统足够强，也足以描述FTA分解的唯一性。他们可以通过将任何一种分解转化为函数产生的标准分解来实现这一点因素定义。这个函数可以被调用正常化，它的工作是将任何一种因子分解转化为标准分解，在标准分解中，质数按顺序排列，并被提升到可能的最高次幂。

其中最著名的现代证明助手是Agda, Coq, HOL, Isabelle, MetaPRL, Minlog, Nuprl和PVS。Nuprl是其中的第一个，创建于1984年，Coq助手是用OCaml编写的，并由INRIA通过法国政府支持。Coq被广泛用于编程。这些证明助手帮助程序员使用自动推理方法检查极其丰富的规范。这些类型足够丰富，足以保证具有该类型的程序对于指定的任务是正确的。这是一种主要形式的正确的构造编程，有时包括从证明规范是可实现的中提取程序的技术;这叫做使用证明的程序．

亚博体育官网研究的目标

一个主要的研究目标是设计类型系亚博体育官网统和编程助手来表达任何计算问题，并提供类型检查机制，亚博体育苹果app官方下载也许通过人工帮助和使用自动推理工具，无论类型系统变得多么具有表现力。

亚博体育官网编程语言、形式化方法和逻辑方面的研究人员正在全世界范围内致力于这个目标。在研究文献中有许多文献引用了这一目标的进展。亚博体育官网亚当·奇利帕拉的新书依赖类型的认证编程麻省理工学院出版社，2013，提供了一个主题的最新观点，重点关注广泛使用的Coq证明助手。西蒙·汤普森1991年的书，类型理论与函数式编程“，这本书是关于这一主题的早期综合教科书之一，因为它刚刚获得了发展势头。Nuprl是自1984年以来仍在使用的最古老的这类证明助手。这在1986年的书中有描述用Nuprl证明开发系统实现数学亚博体育苹果app官方下载．Nuprl文献和2006年前后该领域的概述可以在技术文章中找到"使用Nuprl的计算类型理论创新“从应用逻辑杂志， 4,428 -469, 2006。作者在2010年的一篇关于类型的胜利在2010年的庆典上数学原理在剑桥，英国人讲述了100年前的类型理论，并将其与当前的类型系统研究联系起来，以通过构造程序进行校正。亚博体育官网亚博体育苹果app官方下载可在www.nuprl.org．

当类型系统可以指定安全属亚博体育苹果app官方下载性时，所检查的程序是安全的建设．在正确和安全的构造编程中，规范包括了关于计算环境的假设，比如关于网络拓扑。如果这些假设不成立，比如因为网络拓扑以意想不到的方式改变，那么类型规范就不再足以保证正确性。因此，记录类型规范所依赖的假设是非常重要的。

对于许多问题，这些假设是稳定的，在这些情况下，这种正确性方法是非常有效的。在文献中有很好的例子;在网站上www.nuprl.org我们最近发布了一个简单的例子，目的是向新手说明这个方法。这是一个完整的形式化证明，它允许我们构建一个正确的按构造程序来解决“最大段和”问题，该问题用于教授从类型规范开始的正式程序开发。

最近的工作

作者和他在康奈尔大学的同事最近使用Nuprl创建了一个正确的多paxos分布式共识协议的构建版本，该协议正在数据库系统中使用。亚博体育苹果app官方下载这就需要一个分布式计算的实现理论，这个理论正在稳步发展。我们制定了这个协议attack-tolerant，这是一种安全的形式。共识协议对云计算至关重要，业界努力构建正确的协议，并在修改和改进时确保它们的安全性。亚博体育官网自1984年以来，研究人员已经创建了数百个正确的建筑方案，并通过建筑方案确保安全。在世界范围内，更多的建筑正在建造中。

由于研究的必要性和使用它们的经济动机，现代的证明助手正在逐步变得更加强大和有效，在正确和安全的建设规划。亚博体育官网也有强烈的动机教他们，作为工作软件基础由宾夕法尼亚大学的本杰明·皮尔斯和他的同事证明。证据助手是一项令人上瘾的技术，部分原因在于，使用它们的次数越多，它们就会自我提升，从而稳步提升它们的吸引力和价值。

路加福音:您认为在通常被称为“人工智能”的方法中，应用逐构正确和逐构安全方法的前景如何?

罗伯特。:证明助理例如Agda, Coq和Nuprl，它们支持通过构造编程来纠正错误，这本身就是人工智能的例子，因为它们使用了人工智能中开发的自动推理工具。最早的验证助手，如博伊尔-摩尔验证器，来自爱丁堡大学的人工智能系。在这个领域，有一本影响深远的书，数学推理的计算机建模，艾伦·邦迪(Alan Bundy)在爱丁堡的著作是人工智能领域的里程碑，由学术出版社(Academic Press)于1983年出版。

在适当的时候，这些证明助手也将使用其他人工智能工具，比如那些可以将正式证明翻译成自然语言证明的工具。在这方面已经有了有趣的进展。例如Holland-Minkley, Barzilay和我在16年的论文“Verbalization of High-Level Formal proof”^th1999年全国人工智能会议，277 - 284将数论中的Nuprl证明翻译成自然语言。

这也是这些系统相互使用进行扩展的情况。亚博体育苹果app官方下载例如，现在我的同事Vincent Rahli和Abhishek Anand正在使用Coq证明程序来检查他们想要添加到Nuprl的新规则是否正确，这与他们在Coq中精心形式化的Nuprl构造类型理论的语义模型有关。他们还使用Agda检查了某些规则。这个活动正是你所问的，答案是明确的“是”。

另一方面，当我们着眼于机器学习算法时，它们成功的标准则更加基于经验。他们真的表现得很好吗?Regina Barzilay(麻省理工学院)和Lillian Lee(康奈尔大学)教授在他们2002年的一篇关于“引导词汇选择”的文章中，使用了机器学习算法来提高机器翻译从Nuprl数学到自然语言的性能。对于这类工作，使用正确的构造编程不一定有意义。另一方面，我们可以想象这样一个场景:正确的数学翻译可能是至关重要的。在这种情况下，我们可能不会尝试证明机器学习算法的性质，而是会尝试捕捉自然语言版本的含义，并将其与原始数学进行比较。

“理解自然语言数学”的工作将受益于正确的构造编程。在使用建构类型理论为自然语言理解提供语义基础方面，已经有很好的工作正在进行。这本书是Aarne Ranta，Type-theoretical语法,《1994年的牛津》是这种工作的一个很好的例子。它也是构造类型理论最好的介绍之一。

最终，机器学习算法将对证明助手的有效性产生重大影响。这是因为我们可以通过教它们专家人类如何处理这些任务来提高证明助手独立处理各种子任务的能力。这类工作将是人工智能两方面协同工作的一个很好的例子。机器学习指导机器进行证明，而自动推理工具则检查证明是否正确。

路加福音:您认为在未来10-20年里，证明助手和相关工具会有什么发展?

罗伯特。我从事证明助手、编程逻辑和构造类型理论的工作已经有40年了，其中一部分工作是预测5到7年后的情况，并试图吸引资金来实现一个将推动该领域发展的可行目标。为了保持信誉，你需要在足够的时间里保持正确。在这些预测中，我有8个左右是对的。所以我对未来5到7年的预测很有信心，我对未来10年有想法和希望，然后我对长期有信心。

短期内

在接下来的五年里，我们将会看到更多的正确的例子，比如在构建重要软件的过程中，通过构建程序，以及更多的验证软件系统的例子，比如在seL4内核、SAFE软件栈、英特尔硬件的特性和分布式计算的重要协议方面的工作，亚博体育苹果app官方下载特别是对于云计算。这样做是因为这样做的成本效益越来越高。即使在未来的十年里，我也看不到一个重大的工业努力。这一领域将是持续的学术和工业研究的重点，它将对某些关键系统产生递增的影响。亚博体育官网亚博体育苹果app官方下载然而，对于在工业上广泛部署来说，它仍然过于昂贵。

我们将看到正式的工具被用来使网络战争的进攻性和防御性武器都更加有效。推动这一观点的关键教训之一是，史上制造的最好、最昂贵的武器之一——震网病毒(stuxnet)显然是失败的，因为它存在一个导致其被发现的漏洞。另一个教训是，进攻性武器一直在改进，防御必须更加敏捷，不仅要通过建造“堡垒般的”系统来建立安全，还要把系统看作是学习如何适应、恢复和维护其核心功能的活生生的响应实体。亚博体育苹果app官方下载

在战争领域，成本很少成为决定性因素，与维持一支优秀军队所需的其他成本相比，正式的方法工具的成本并不高得离谱。在这个领域，不像建造和维护船只、飞机、火箭和防御它们，成本在于培训和招募人员。这些人也将拥有私营部门的宝贵技能，而私营部门仍将渴求受过良好教育的人才。

因此，总的来说，投资于先进的正式方法技术将被视为具有成本效益。证明助手是我们在这一领域拥有的最好的工具，我们知道如何通过投资使它们变得更好。这些工具包括合成方面的Agda、Coq、Nuprl、Minlog和MetaPRL，以及验证方面的ACL2、Isabelle-HOL、HOL- light、HOL和PVS。它们都很好，每个都有重要的独特特点。他们都作出了重大贡献。他们都有雄心壮志，希望在自己最擅长的领域变得更有效率。它们将吸引更多的资金，新的系统也将出现。亚博体育苹果app官方下载

中期

目前大部分的证明助手也被用于教育。在我看来，很明显，与编程语言很好地集成在一起的证明助手，如Coq与OCaml和ACL2与Lisp，将会因为在编程课程中使用而繁荣起来。其他的证明助手也会朝这个方向发展，Nuprl肯定会这么做。教育领域会发生什么，将取决于将编程语言引入或淘汰大学的力量。在我看来，Coq/OCaml系统将有机会在大学教育中被广泛采用，至少在欧洲和美国亚博体育苹果app官方下载是这样。它已经对常春藤联盟产生了重大影响——康奈尔、哈佛、普林斯顿、宾夕法尼亚和耶鲁都有投资，MIT也是。我预测，在五年内，我们将在mooc中看到这种编程教育，我们将看到它进入一些精选的大学和顶尖的高中。

所有的证明助理都有一些特殊的专业领域。如果有足够的资金，我们将看到他们利用这一点，并向各个方向推进他们的系统。亚博体育苹果app官方下载Nuprl已经非常有效地构建了正确的分布式协议，同时也具有攻击容错性。这项工作很可能会继续下去，并最终在编程语言中构建通信原语，以匹配已经正式发展的事件理论。Coq已经被用来构建一个经过验证的C编译器，在宾夕法尼亚大学和哈佛大学，Coq被用来验证用于支持安全特性的新硬件的Breeze编译器，在麻省理工学院，他们正在使用Coq与Bedrock系统验证更多的软件堆栈。亚博体育苹果app官方下载Coq的其他应用不胜枚举。我们将看到更多的努力来正式证明数学中的重要定理，但很难预测是哪个和由哪个系统来证明。亚博体育苹果app官方下载目前在同伦理论中使用证明辅助的努力将继续下去，并将产生重要的数学见解。证明助手还将支持沿着Kurt Mehlhorn令人印象深刻的工作路线构建更多认证算法的努力。

长期

第一次见到由世界级专家操作的鉴证助手的人很可能会感到震惊和震惊。这种人类/机器的伙伴关系可以做一些看起来不可能的事情。他们可以完全精确地实时解决某些数学问题，在Latex中留下可读的正式证明，作为一小时工作的记录。整本书都是以这种方式写成的软件基础宾夕法尼亚大学的一个项目。我预测，我们将看到更多以这种方式出版的可读的正规数学和计算理论书籍。在他们的周围将出现一种技术，以促进这种写作，并将其纳入广泛分发的教育材料。或许可以使用证明助手来给mooc的家庭作业打分。此外，使用证明助手迟早会到达高中。

我认为，我们还将看到新型的远程研究合作，由证明助手进行中介，并在互联网上共享。亚博体育官网我们将看到世界各地的联合研究团队攻击亚博体育官网某些类型的理论问题，并通过构建构建出正确的整个软件系统。亚博体育苹果app官方下载我们已经在Coq、Agda和Nuprl社区看到了这一点，在那里，证明助手分享了非常相似和兼容的类型理论。

在很长一段时间内，可能有一种更大的力量在发挥作用，一种自然的力量，将传播和保存信息的机制编码到人类基因库中，这些信息定义了我们的物种。我们可能不会智人毕竟,但人类informatis．智慧的比特并不总是如此明显，但信息比特的进展还不错——至少到目前为止是这样。这就是我们人类的一面，我们为此建立了证明助手伙伴。它们是不断扩张的信息生态系统的一部分。亚博体育苹果app官方下载有可能进一步进化的证据助手将被自然界视为我们的一部分。

路加福音:谢谢你,鲍勃!