Cheng Tan

那笔旧交易

形式化方法交付确定性，只是用一门没几个工程师书写或阅读的语言

· systemsresearchai

2009 年，NICTA 完成了对 seL4 操作系统内核的证明。这个内核是 8,700 行 C 和 600 行汇编；它的 Isabelle 证明是 200,000 行。造这个内核花了大约 2.2 人年，证明它花了大约二十人年。两年前，CompCert 已经为一个 C 编译器做过同样的事：42,000 行 Coq——如今叫 Rocq——其中 76% 是”编译保持了你程序的语义”这一证明。再往后，IronFleet 验证了两个分布式系统，并报告了一个本该更出名的细节：两个系统第一次跑就是对的。

这不是一个关于失败的故事。这是一个在某条边界之内彻底成功、而那条边界从未挪动过的故事。几乎所有软件都写在它之外。成本解释了其中一部分；剩下的，看清霍尔逻辑到底在做什么就容易看见了。

那些规则做了什么，又悄悄地没做什么

霍尔逻辑用一个三元组：前置条件、程序、后置条件。它的规则描述程序如何组合：顺序、赋值、循环。它们小巧而优雅。然后是推论规则：如果一个程序建立了 R，而 R 蕴含 S，那么它也建立了 S。

看第二个前提。那个蕴含并不是关于程序的事实。它是关于断言语言的事实，而霍尔逻辑并不证明它。它假定有别人能做到。程序规则提供结构；数学内容坐在那些附带条件里。

库克在 1978 年把这一点说精确了。霍尔逻辑不可能彻底完备——理由要追到塔斯基，而不是工程——但它是相对于某个神谕完备的：只要允许你在证明途中去查询”所有真断言”这个集合并得到答案，它就是完备的。这门学问的标准史述把这个动作描述为：把真断言当作一个”可以在正确性证明中随意查询的神谕”。

于是谓词逻辑是子例程，霍尔逻辑是调用约定；验证一个程序时所有难的东西，都难在断言语言里，而不在包着它的那层程序逻辑里。五十年的工具建设，实际上就是五十年在造更好的神谕：判定过程、SMT 求解器、策略语言、证明自动化。调用约定从未变过。

两张账单，而第二张更糟

看得见的那张是证明的工作量，人人都在引用它。二十人年对两人年。文件里的 76%。IronFleet 费了大力气，把它实现层的比例压到每行可执行代码配 3.6 行证明标注，这是一项实打实的成就，而它仍然是 3.6。

更安静的那张是规约，它不好逐项开列。在这一切开始之前，必须有人用逻辑写下这个系统应该做什么，而没有任何东西检查那句陈述。它是顶上的那条公理。IronFleet 的作者对此很直接：IronRSL 的可信规约是 85 行，IronKV 是 34 行，”使它们易于被检视其正确性”。易于检视，由一个人，读它。

世界上每一个被验证过的系统，最顶上都有一段话，是某个人读过并且相信了的。

seL4 把周界的其余部分划得很仔细：”我们假定编译器、汇编代码、启动代码、缓存管理与硬件是正确的；其余一切我们都证明。”这是一条划得干净、也划在明处的线。但同一篇论文里还有一句更安静的话，关于内核自己的虚存窗口：”我们只是非形式地给出了这个一致性论证；我们的模型并不强制我们去证明它。”即便在机器检查的系统软件所能达到的最高水位线上，仍然有一道接缝：证明在那里停下，然后一个有能力的人说一句显然。

验证不是消息

1979 年，德米洛、利普顿与佩利斯预言程序验证注定失败。他们错了，这一点值得先说：seL4 在那儿，CompCert 已经装进了航电工具链，三十年间读过他们文章的人所做的工作驳倒了这个预言。

活下来的是预言底下的那个观察。数学证明是靠社会过程赢得信任的：它被阅读、被复述、被讲授、被怀疑、被修补，最终被吸收。程序验证进不了这个过程，因为它就是那么个东西：

验证不是消息；一个人若冲到走廊上去宣告他最新的一份验证，会很快发现自己成了社交弃儿。

还有更直白的一句：”验证冗长、缠绕，却浅薄；毛病就出在这儿。”一份 200,000 行的 Isabelle 脚本是一张有价值的证书。你可以检查它，而这份检查价值极大。但你没法读它，没法只对其中一部分表示异议，没法在设计评审上引用它，也没法拿它向一个新来的工程师说明这个内核为什么安全。知识存在，却不流通。

他们也看见了规约问题，那句话四十五年来一个字都不用改：”任何一个像样的编译器或操作系统，它的规约都能写满好几卷——而没有人相信它们是完整的。”

条款

把你的本意翻译成一门形式断言语言，机器就会以确定性检查这次翻译下游的一切。

这是一笔好交易，支持它的证据压倒性地多。但注意你付出的是什么，因为这两笔开销都不会随规模下降。你首先得有能力完成这次翻译，这就排除了所有你能用自然语言说清、却没法用逻辑说清的性质，而这样的性质很多。而拿回来的是一张证书，不是一份同事跟得下去的论证。

所以验证集中在赌注付得起它的地方：内核、编译器、密码学、飞行控制。别处呢，正确性论证照样每天用自然语言做出来，不停地做，而没有任何东西检查它们。

下一个问题不是怎么把形式证明变便宜。而是：当断言语言变了，会发生什么。

参考文献