为什么GCC能被验证，而PDF却不行？
Specifications Don't Exist (2025)
文章指出，形式化验证的瓶颈往往不在于证明过程，而在于规格说明的缺失。对于GCC编译器或SeL4微内核，我们拥有清晰的数学定义，验证虽昂贵但可行。然而，像Chrome浏览器或PDF格式这样的系统，由于缺乏精确且统一的规格说明，甚至可以说“规格说明根本不存在”。现实中充斥着大量模糊、矛盾的非正式文档，导致系统行为处于灰色地带。即使未来AI让证明变得廉价，若无法明确“我们要什么”，形式化验证依然寸步难行。
规格说明并不存在——我指的不仅仅是没人写过它们，而是我们有理由相信根本无法写出精确且连贯的规格说明。
HN 评论区
13- ivanbakel
关于规范撰写的观点非常中肯。有时候，形式化验证的研究就像醉汉在路灯下找钥匙，目标领域往往恰好适合用某种特定的计算机科学方法去处理。
不过，我认为在“天然可验证”和“困难案例”之间存在一个中间地带。某些领域，比如银行应用，确实需要关于 UI 行为的正确性保证。一个封闭的应用可以非常规范，因此理论上像“用户执行了此操作并确认”这样的规范可以变得有意义。但将规范与 UI 绑定是一件棘手的事，而且显然比函数边界更容易变动——应用会经历重新设计，样式和元素会移动等等。将 UI 抽象为状态机并不难想象，但真正将规范挂钩到程序中本身就是一个大问题，而常见的应对方式就是干脆忽略这些棘手的领域，转而做一些更简单的事，比如编写不需要处理那些非编程语言（PL）形态问题的后端规范。
- mad44
现在已经有像 Specula 这样的项目，利用 LLM 让我们能够从实现中推导出规范，并且有些悖论的是，又利用这些规范来发现实现中的 bug。
https://muratbuffalo.blogspot.com/2026/08/specula-scaling-fo...
其次，我认为开放的、可组合的部分规范（open partial specs, composable specs）有助于解决 Dodd 所提到的单体规范（monolithic specs）的问题。
https://muratbuffalo.blogspot.com/2026/08/composition-and-mo...
- tel
过去几个月我一直在开发一种类似 Markdown 的轻量级文档格式。（简单介绍一下，它像 Markdown，但内置了自然的扩展点，且歧义少得多）。
我的一个主要目标是编写该格式的“规范”。我希望它足够好，以至于用户可以正当地针对我的主要实现不符合规范而提交 bug 报告：它就是关于该语言的权威来源。
所以，当然，讨论“耸耸肩，也许这样是对的”这种灰色地带让我觉得非常有趣。整个过程一直驱使我去做两件事：(a) 让语言本身具有弹性和包容性，以便对几乎所有的文档都能给出某种答案；以及 (b) 限制系统的输出，使其尽可能丢弃信息，从而让我们能更自信地对语义做出断言。
我不知道我能否实现所有的目标。这算是一个小项目，肯定比（比如）网络浏览器简单得多。但与此同时，要真正聚焦于我到底希望这样的规范说明什么，是非常困难的。