Coq

概述

Coq 是法国 INRIA 主导开发的交互式定理证明助手,始于 1984 年,理论基础为归纳构造演算(Calculus of Inductive Constructions)。用户以其规格语言 Gallina 书写定义与命题,借助策略(tactic)语言交互式构造证明,内核负责最终校验。2025 年项目宣布更名为 Rocq。

原理

Coq 建立在 Curry-Howard 同构之上:命题是类型,证明是程序,微小的可信内核逐项检查证明项,保证只要内核正确、被接受的定理即可信。其提取机制可把验证过的函数导出为 OCaml、Haskell 代码。

标志性成果

四色定理(Georges Gonthier,2005)与 Feit-Thompson 奇阶定理的机器化证明、经形式验证的 C 编译器 CompCert、微内核与密码学库的验证等,使 Coq 成为形式化方法最具代表性的平台之一,团队曾获 ACM 软件系统奖。

评价

Coq 生态成熟、教材丰富(如《Software Foundations》);批评集中于策略脚本可读性与学习成本,新兴的 Lean 在数学形式化社区形成了有力竞争。