为什么写出正确的软件这么难：可计算性给出的硬边界
来源：pron.github.io — 2026-11-12
📋 概述
这篇长文把软件正确性当成数学问题来讨论：从希尔伯特纲领、哥德尔不完备与图灵停机问题讲起，再进入复杂性理论的结果，论证程序与完整理解在根本上相互冲突。作者的目的不是劝人放弃验证，而是把散落在文献里的结论集中到一处，反驳「有了对的工具，正确性就唾手可得」的说法。他的落点是：正确性有代价，这个代价像减少熵所需的能量一样，来自计算的自然规律，绕不过去。
🔑 核心要点
- 论证顺序清晰：先说明完全理解一个程序在一般情况下不可判定，再说即便可判定，代价也可能高到无法承受。
- 作者来自实践：文章源于他为 Galaxy 做形式化规格与验证时踩到的复杂性结果，不是纯理论综述。
- 他对工具的态度不是否定，而是校准预期：工具有用，但不能改变成本的量级。
- 全文约四十五分钟阅读，附有讲稿之外的额外证明与脚注，适合当参考资料而不是爽文。
💡 金句
The cost of correctness - like the energy cost of reducing entropy - is a result of the natural laws of computation, that cannot possibly be avoided.
👍 0
👎 0
← 返回 Hacker News 首页