The Case Against Formal Verification, 50 Years Later

文章重访 DeMillo、Lipton 与 Perlis 近 50 年前的批评：数学证明的可信度还来自同行反复阅读、争论和形成共识，大型程序证明很难自动获得同等社会审视。现代证明助手能检查内部推导是否符合规则，却不能自行保证规格写对、模型覆盖现实或组织会持续维护证明。它反对的不是形式工具本身，而是把机器验通过度外推为整个软件系统已被证明正确。