50年后，形式化验证真的赢了吗？

The Case Against Formal Verification, 50 Years Later

随着AI编码的兴起，形式化验证正从边缘走向主流，Google Trends搜索量激增，Lean等工具被广泛学习。然而，1979年一篇经典论文曾断言程序验证注定失败，无法提升人们对程序的信心。本文重读这篇50年前的文章，逐一分析其六大论点：从证明的社会属性、规范与实现的脱节，到全自动验证的不可行性，再到现实系统的复杂性。作者指出，虽然全量验证并非万能，但在AI生成代码的时代，精确描述意图和验证正确性变得前所未有的重要。形式化方法不再是魔法棒，而是提升软件可靠性的关键工具之一。