为什么 Rocq 比 Lean 更适合程序验证
来源：joomy.korkutblech.com — 2026-07-31
📋 概述
尽管 Lean 在 AI 辅助数学证明方面表现出色，但作者认为 Rocq（原 Coq）在程序验证方面仍然更胜一筹。关键差异在于：Rocq 原生支持余归纳类型和具有可执行语义的 cofixpoint，而 Lean 的方案仅支持谓词层面的余归纳。此外，相互余归纳声明在 Rocq 中是常规操作，在 Lean 中则缺乏支持。
🔑 核心要点
- Rocq 原生支持 CoInductive 和 CoFixpoint，可提取为可执行程序；Lean 的 coinductive 仅限于谓词层面。
- 相互余归纳类型在 Rocq 中直接可用，Lean 的 QPFTypes 库明确标注为"概念验证"且不支持。
- 作者强调这种区别仅针对程序验证——在数学形式化方面，Lean 确实有实际优势。
- QPFTypes 甚至不支持无参数的余数据类型，而这是 Rocq 中的基本操作。
💡 金句
我需要的是 Type 中的 codata，是我真正可以运行的东西。Rocq 直接给了我这个。
👍 0
👎 0
← 返回 Lobsters 首页