Coq（Rocq）

定义

Coq 是由法国 INRIA 主导开发的交互式定理证明器与依赖类型函数式语言，理论基础是归纳构造演算（Calculus of Inductive Constructions）。项目于 2025 年前后更名为 Rocq。

工作方式

用户以 Gallina 语言书写定义与命题，用策略语言（tactics）逐步构造证明，内核对每个证明项做类型检查，保证结论可靠。通过程序抽取（extraction）功能，可将验证过的函数导出为 OCaml、Haskell 等语言代码。

代表性成果

四色定理与 Feit-Thompson 奇阶定理的机器化证明、经过完整验证的 C 编译器 CompCert，都是在 Coq 中完成的标志性工程。

意义

Coq 是形式化数学与高可信软件验证领域最有影响力的工具之一，也深刻影响了 Lean、Agda 等系统的发展。