为什么 Rocq 比 Lean 更适合程序验证
来源：joomy.korkutblech.com — 2026-07-30
📋 概述
作者从程序验证的角度系统比较了 Rocq（前 Coq）和 Lean 两个证明助手。尽管 Lean 在数学形式化领域势头强劲，但在程序验证方面，Rocq 提供了 Lean 所缺乏的共归纳类型原生支持、可执行的共不动点、以及成熟的代码提取能力。Lean 的 codata 支持仍处于概念验证阶段，无法处理互递归或索引类型的共归纳声明。
🔑 核心要点
- Rocq 原生支持 CoInductive 和 CoFixpoint，可直接提取为 OCaml 惰性值
- Lean 的 codata 支持通过 QPFTypes 概念验证库 实现，无法处理互递归和索引类型
- Rocq 的共不动点可 提取为实际运行的 OCaml 代码，Lean 缺乏等价能力
- Lean 4.25 新增 coinductive 谓词但 不提供可执行程序或代码提取
- 对于需要共归纳的协议验证和状态机建模，Rocq 仍是更好的选择
💡 金句
这不是在挑起论战——如果你比我成熟，请自动将'更好'替换为'对我今天的工作更适合'。
👍 0
👎 0
← 返回 Lobsters 首页