文章作者解释了自己不使用依赖类型的原因，指出证明对象在类型理论中虽常见但非必要，且会占用大量空间。他提到50年前Robin Milner提出的LCF架构通过实现语言进行类型检查，确保证明步骤合法。作者表示自己曾多年使用依赖类型，并以1977年与de Bruijn的交流经历为例。

标题：为何不采用依赖类型？——一位形式化验证先驱的思考

核心内容提炼：

本文作者回顾了其数十年在定理证明器领域的探索历程，阐释了Isabelle系统放弃依赖类型（dependent types）与证明对象（proof objects）的设计哲学，并比较了不同类型理论在数学形式化中的优劣。

1. 设计哲学溯源

• LCF架构的启示：50年前Robin Milner提出的LCF架构证明内核理念，通过实现语言的类型检查确保证明步骤合法性，无需冗余的证明对象。
• AUTOMATH的影响：1977年作者师从de Bruijn学习AUTOMATH系统，虽未实际使用，但其"逻辑框架"理念（支持多种形式系统）深刻影响了Isabelle的通用性设计。de Bruijn反对过度复杂的类型理论，这一立场与Isabelle追求轻量级的理念相契合。

2. 类型理论的实践探索

• Martin-Löf类型理论阶段：作者曾投入数年研究该理论，甚至初版Isabelle即基于此实现（现仍保留为Isabelle/CTT）。但因该理论转向"内涵相等性"导致前期工作作废，且对其教条化倾向产生抵触。
• 构造演算的质疑：面对Coq/Lean等基于构造演算的系统，作者始终持保留态度，认为其理论基础不断演变，存在"可选公理"的随意性。

3. 高阶逻辑的胜利

• 历史性选择：Mike Gordon等人在1985年即用Church的简单类型理论验证硬件，证明经典方法仍具生命力。Isabelle/HOL通过类型类和locales等扩展，突破了传统高阶逻辑的限制。
• ALEXANDRIA项目的突破：在代数闭包、格罗腾迪克概形等高级数学的形式化中，高阶逻辑展现出意想不到的表达力，打破了"依赖类型不可替代"的迷思。

4. 现状反思

• 工具生态对比：作者承认Lean社区在数学库规模（mathlib）和蓝图工具（Blueprint）上的优势，但指出其性能问题和依赖类型的实践困境（如与内涵相等性的冲突）。
• 终极结论：依赖类型如同特斯拉"全自动驾驶"——看似美好但需谨慎对待，其真正价值在于"知道何时不用它们"。

删减说明：

• 移除个人回忆性细节（如与de Bruijn的私人交往）
• 简化技术术语的学术史溯源（如Curry-Howard对应的争议）
• 合并重复论点（如对不同类型理论"正确性"的多次讨论）

保留的关键细节：

• AUTOMATH作为"逻辑框架"的餐厅比喻
• Martin-Löf理论转向对作者工作的具体影响
• 代数闭包定理形式化的里程碑意义
• 对Lean社区成就的客观评价

以下是评论内容的总结，涵盖主要观点和论据，并保持不同观点的平衡性：

1. 依赖类型的适用性与局限性

• 支持有限使用：依赖类型在特定场景（如矩阵类型、精细索引不变量）中有用，但多数情况下HOL（高阶逻辑）加类型类和局部定义更高效。

  • fluffypony: "For the other 95%, HOL plus type classes and locales... will get you to production faster."
  • anonzzzies: "You just prove / use dependently typed languages / tla+ where it makes sense, not for everything."

• 复杂性与调试困难：依赖类型可能导致类型检查错误与证明错误的混淆，增加调试难度。

  • lacker: "When you make an error in a proof, it's understandable if it's very complicated... The natural UI is different."
  • Gajurgensen: "Dependent types are best used as little as possible... due to issues with heterogeneous equality."

2. 工具与社区的影响

• 自动化与库的重要性：工具链的自动化、库的丰富性（如Lean的mathlib）比核心演算的先进性更关键。
  • fluffypony: "What moved the needle was automation, libraries, and legible proofs, not a fancier core calculus."
  • lacker: "Lean's library... is organized like an open source community... whereas Isabelle's AFP is like a scientific journal."

3. 逻辑强度与数学表达

• HOL的局限性：简单类型理论在逻辑强度上不足以表达现代数学（如范畴论中的规模问题）。
  • cwzwarich: "Simple type theory is equivalent in logical strength to bounded Zermelo set theory... too weak for post-WW2 mathematics."

4. 实际应用与创新

• 数据库与查询优化：依赖类型与数据库查询结合（如TypeDB）可提升复杂数据应用的效率。
  • obeavs: "Combining dependent types with database/graph queries... reimagines how you think about querying databases."

5. 证明对象的价值争议

• 证明对象的必要性：部分认为证明对象冗余，但反射证明（如四色定理）依赖它们。
  • stevan: "Proof by reflection relies on proof objects... Georges Gonthier's four-colour theorem uses it."
  • zozbot234: "Proof terms with opaque 'holes' could replace full proof objects via LCF-like scripts."

6. 美学偏好与实践权衡

• 主观选择：部分争论源于美学偏好，实际优势不明确时更依赖个人选择。
  • pron: "Much of the debate boils down to aesthetic preferences... if there were overwhelming practical advantages, there wouldn’t be much to debate."

7. 极端观点

• 否定价值：个别评论认为依赖类型投入产出比低。
  • golemotron: "The juice isn’t worth the squeeze."

总结

评论普遍认可依赖类型在特定场景的价值，但强调其复杂性、工具链效率及社区支持的重要性。HOL等替代方案在多数场景更实用，而逻辑强度和创新应用（如数据库）展示了依赖类型的潜力。争议焦点集中在证明对象的必要性和美学偏好上。