基于词元的形式化方法

工程师每天都在做正确性论证：这次重试是安全的，因为处理函数是幂等的；这个队列不会无界增长，因为生产者会阻塞在同一把锁上；窗口里永远不会出现重复字符，因为我们会把左边界移过每一次重复。它们出现在设计文档里、代码评审里，以及那些棘手循环上方的注释里。它们才是真正让软件得以运转的推理，而它们几乎从来不是用布尔逻辑写下的。

这有点尴尬，因为形式化方法花了五十年，把”检查正确性断言”这件事做得非常好。它们证明过内核、编译器和分布式协议，而那些证明是立得住的。但它们检查的，是用形式语言写下的论证；上面那几句不是。

这个系列要问的是：这道缝隙能不能从另一头弥合。与其把人翻译成求解器的语言，我们能不能让寻常的工程论证就以它本来的样子变得可检查？

论点

一段自然语言的论证，可以像程序证明那样被检查。把它拆成小步：两三条前提，一条结论，一次熟悉的推理。给每一步标明它用到什么、产出什么。结果是一张证明图。它的节点可以一个一个地检查，它的接线可以由普通代码检查；而当某处出错时，指向的是某一条具体的断言，而不是整篇文档。

底下那个动作比听上去要窄，而我认为它正是读懂当下这一波工作的正确角度。霍尔逻辑从不证明程序证明里的那些蕴含式；它的推论规则把它们交给了断言所用的那门语言。五十年来，被委托的一方一直是某种判定过程——一个求解器，一套策略库，十年的自动化。把它换成一位读者，这条路线的许诺与风险，你就都继承下来了。

为什么是现在

因为代码的生产方式变了。

一个智能体几分钟就能给你一份能跑的 diff。它给不出的，是它权衡过哪些别的方案、它当时握着哪条不变式、边界情形为什么是安全的。那些推理有时没被写下来，更多时候根本没有以任何可供审视的形式存在过。你继承了代码，却没有继承它的论证。

测试补不上这道缝隙，因为它从来就没补上过。一套测试报告的，是某个人想到要写的那些情形。这从来都是局部的证据，而它从来也够用了——不是因为这个样本好，而是因为样本从来不是全部理由。还存在一个作者，他能解释这个设计；还存在一个评审者，他能掂量这份解释。那枚绿色的对勾，是对一份住在别处的论证的旁证。随着代码越来越便宜、它的作者越来越找不着，那枚通过的测试就被要求去承载它承载不了的信任。

这个系列包含什么

那笔旧交易审视形式化方法交付了什么、又收取什么：二十人年的证明对上两人年的内核，一份没有任何东西检查的规约，以及一张没几个人读得下去的证书。
词元逻辑保留霍尔的结构，换掉断言语言。它为小步子辩护，并指出那个同一的组合动作如何分别现身为亚里士多德的中项、根岑的切规则，和霍尔逻辑里的顺序。
它管用吗？用一个算法和一个被植入的 bug 来试这个想法，看看眼下两个在规模上尝试此路的系统，并梳理关于这位裁判有多可靠的已知证据。

最后落在哪里

这东西不取代 Rocq、Lean 或 SMT 求解器，造它的人也不这么宣称。

最后一章里的实验是刻意做小的：十五行代码，证明两遍——一遍是十六个自然语言步骤，一遍是 445 行经机器检查的 Rocq。那张图后来成了形式证明好用的提纲。它预言了难点会落在哪里。而当代码被动了手脚，失败恰好落在那个节点上——它自己的理由里，早已点名了那个关键的守卫条件。

它能站得住的结果是否定的那一个：这一步断了，而这个输入证明它断了。反例是事实，因为程序真的跑过了。而一个肯定的判决是一摞可能出错的判断，一摞判断的好坏，取决于其中最差的那一个。这个限度是真的，我宁愿把它直说，也不绕着它讲。剩下的东西仍然值得拥有：一份可读的论证，它在一个说得出名字的地方失败，而它所关于的那个断言，是用它作者真正在用的语言说出来的。