交互式定理证明工具 Coq 的产生与发展（转）

本文转载自科学网——王小平的博客

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the formalization of programming languages semantics (e.g. the CompCert compiler certification project or Java Card EAL7 certification in industrial context), the formalization of mathematics (e.g. the full formalization of the 4 color theorem or constructive mathematics at Nijmegen) and teaching.

1970 年代：Gérard Huet 开始在自动定理证明方面进行工作，使用 LISP 语言实现了带等式的一阶逻辑证明器 SAM。λ 演算成为研究证明论的主要工具。Jean-Yves Girard 证明了分析的一致性，他的证明使用了称为 System-F 的多态 λ 演算中证明的终止性。这一系统被推广到一个表示多态泛函的 Fω 系统，因而可为一类超出了传统序数层次的算法进行编码。John Reynolds 在推广 ML 语言的受限制的多态结构时，又重新实现了这一系统。

1980 年代：Knuth 和 Bendix 开展了奠基性研究工作。Jean-Marie Hullot 和 Gérard Huet 完成了一个 KB 软件，它以一种自然的方式实现代数结构的自动判定过程和半可判定过程。同时，归纳证明领域也取得了稳步的进展，最著名的工作是 Boyer 和 Moore 的 NQTHM/ACL 系统。同时，逻辑学家（Dana Scott ）和理论计算机科学家（Gordon Plotkin 、Gilles Kahn、Gérard Berry ）正在研究可计算函数的一种逻辑理论（可计算论域），以及有效可用公理化（可计算归纳），目的是为了定义程序语言的语义。Gérard Huet 联合巴黎高等师范学院的 Guy Cousineau 和 Pierre-Louis Curien 在 INRIA Rocquencourt 实验室启动了 Formel 项目。他们准备把 ML 语言不仅用于定义 tactics，同时用于实现整个系统。这一项在函数式方面的研究和开发工作在几年后产生了 CAML 语言族，最终导致了今天的 Objective Caml 语言，它就是现在的 Coq 证明器的实现语言。1984 年，Gilles Kahn 在 Sophia Antipolis 组织了一个类型理论的国际会议，在会上，Thierry Coquand 和 Gérard Huet 展示了一个把依赖类型和多态类型综合在一起的系统，它把 MartinL.f 的构造性理论融入了 Automath 系统的一个扩展，该系统命名为构造演算（Calculus of Constructions）。1989 年，Coq 4.1 版本发布，该版首次加入了由 Benjamin Werner 所设计的从证明中抽取函数式程序（Caml 语法）的机制。

1990 年代：推出的 Coq 5.6 版提供了进行数学描述的统一语言（Gallina“vernacular”），原始归纳类型，从证明中抽取程序的机制，和一个图形化用户界面。1996 年 11 月发布的 Coq 6.1 版引入了所有上述理论成就，也包括了几项对提高效率有关键作用的技术，特别是 Bruno Barras 的规约机制，

2000 年以后：Coq 系统经历了完全的重新设计，版本 7 拥有一个函数式核心，主要架构师是 Jean-Christophe Filli.tre，Hugo Herbelin 和 Bruno Barras 。一个用于 tactics 设计的新语言由 David Delahaye 开发出来，此后人们可以用高级语言为复杂的证明策略编程。为了对数值软件进行正确性验证，Micaela Mayero 研究了实数的公理化问题。同时，Yves Bertot 重新利用 CtCoq 的思想，用 Java 语言开发了一个复杂的图形界面 PCoq 。2002 年 Jacek Chr.aszcz 采用了类似 Caml 的方法把模块和函子系统整合在一起。2003 年底，在经过对主要的输入语言进行重新设计之后发布了 8.0 版本（目前版本 8.4）。目前在应用方面，Coq 已经足够强壮，并可用作实现特定证明工具的低层语言

Coq 迄今最为成功的应用在软件形式化验证方面。Trusted Logic 利用 Coq 成功地完成 JavaCard 语言的整个执行环境的形式化验证。这项安全方面的工作获得 EAL7 证书奖（公共标准下最高级别的奖励）。开发使用了 121000 行 Coq 代码，总共 278 个模块。2013 年 Coq 获得 ACM SIGPLAN 编程语言软件奖。此外，Coq 在数学定理辅助证明方面也有不少斩获，如“四色定理”证明（这样是否意味了数学和计算机变成真正的一家亲，天才的数学家们是否担心害怕自己的饭碗问题呢？随着计算机能力的快速增长， 再过二三十年， 大多数研究都将可以由计算机来做。 它们不仅能证明数学定理， 甚至可以发现数学定理，但就目前两个学科的发展现状而言，计算机至多只能起辅助作用，还不能代替人创造性的思考）。

值得关注的是，另一种基于高阶逻辑的定理辅助证明系统 Isabelle 也在研究和发展中，它进行函数式程序建模，多数证明只要两步完成：对所选变量进行归纳以及使用自动策略，能够处理集合、函数、关系以及实现递归定义集合，利用了嵌套递归和交叉递归等技术、大量可供选择使用的低级证明策略。

参考文献：

Coq 官方网址

Coq 维基百科

(德)Yves Bertot Pierre Casteran 著，顾明 译。交互式定理证明与程序开发—Coq 归纳构造演算的艺术。清华大学出版社，2010 年