前几天看到一篇文章，讲 AI 生成代码最大的风险不是烂，是“能运行但不正确”——代码跑得起来，测试全绿，安静地解决着一个没人要它解决的问题，在生产环境里一趴几个月没人察觉。这个区分抓得准：坏代码会喊疼，报错、崩溃、测试挂掉，全是显性的；错代码不吭声。评论区一位叫 UnitBuilds 的读者讲了个更瘆人的例子：AI 生成的单元测试，测的不是给定的变量，而是它自己生成的样板代码，测试全过，应用一跑全是错。他管这叫“自我满足的系统”。这个词我打算借用一下，因为它给这整类问题起了名字。
这类讨论的默认语气都是“AI 带来了新问题”。我想把年份往前拨。
1968 年 10 月，西德加米施，NATO 那场软件工程会议，“软件危机”这个词就是从那儿叫开的。留下的论文集里满篇是同一个焦虑：验证跟不上生产，积压的待测工单堆得没人看得完。评论区有位读者说，人从 1960 年代起就被待测工单压垮，LLM 只是让老症状更显眼，这句我认。病不是新的，宿主换了。
会议之后，学界下过一个很大的注。1967 年 Floyd 的《给程序赋义》，1969 年 Hoare 在 CACM 上的《程序的公理基础》，路线一致：给程序证明正确性，让“对不对”从观点变成数学。Dijkstra 那句被转引了半个多世纪的话，测试只能证明 bug 存在，不能证明 bug 不存在，出处就是他 1968 到 1970 年间那几份结构化编程讲义（各家转引的措辞出入不小，意思没跑）。这条路最后没铺开，原因不体面但简单：写一份足够精确的形式规格，成本不比写程序本身低，而规格自己也可能写错，付得起这个钱的只有航天军工那一小撮。形式验证没有输给对手，输给了账单。我承认我对那拨人有偏爱，但偏爱改变不了他们没赢的事实。
那业界实际靠什么验证“这是不是对的问题”？靠人。1976 年 Fagan 在 IBM 把 code inspection 制度化，同事坐一屋读代码，规格里含糊的地方在人眼皮底下过一遍；往后二十年各团队变体无数，骨架一样：意图验证烧的是人的注意力，贵，慢，但它是唯一在跑的机制。
到了九十年代末，Kent Beck 那拨人给 Hoare 交了个实用主义的翻译：证明不了，就把规格写成能执行的代码，测试先行。1997 年 Beck 和 Gamma 搭出 JUnit（据传初版是在去 OOPSLA 的飞机上敲的），再往后 CI 起来，流水线把“绿了没”变成每次提交都要问的一句话。这一步是分水岭，但分水岭的代价当时没人标价：流水线回答的是“跑起来没有、测试过没过”，“这是不是对的问题”仍然外包给人，code review、旁边的同事，还有一件从没人记账的事：写代码的过程本身。
这件事值得单独拆开。人手写代码的几十年里，实现过程一直在顺手干一件没被承认的活：逼你把需求想清楚。写到一个含糊处，你得停下来问“这里到底要什么”，一问，规格的窟窿就露出来了。评论区 Dirk Mattig 那句说得很硬：“搜索功能”不是一个需求，是一个需要规格说明的功能。人写代码会在半路撞上这句话；AI 不会。它按字面把“搜索”实现成精确匹配，把带祖父条款的业务规则压平成主流程，把边缘情况全按乐观路径处理——不是它蠢，是团队脑子里的默认知识没写进提示词，而它填窟窿的方式是挑一个看起来合理的默认值。人填窟窿靠语境和善意，模型填窟窿靠合理的样子。这就是“结构上匹配提示”和“解决真实问题”是两回事的机制。摩擦没了，验证也没了，这笔账以前从没单独开过，因为它藏在打字里。（这里其实还牵扯到需求文档为什么从来写不全，那是另一条线，按下不表。）
更麻烦的是测试那边同时失守。测试理论里有个老概念叫 test oracle：你的“预期结果”从哪来。它的价值从来有一半在独立性，预期不能从被测的东西里长出来。作者自己写的测试常和代码共享同一个误解，这是老病；AI 生成代码再顺手生成测试，是同一个误解的自动化量产。全绿的流水线证明的只是自洽，不是正确。那位追了几个月 97.2% 覆盖率的读者，最后想明白的也是这层：覆盖率量的是代码被执行的比例，不是被执行的是不是对的东西。顺带一句考据：那句“指标一旦成为目标就不再是好指标”，流行版措辞其实出自人类学家 Strathern 1997 年一篇讲英国大学审计的文章，大家记成了 Goodhart 本人说的，连吐槽指标的话本身都是个转引事故。
所以这轮讨论里我最不同意的声音，是“AI 太按字面理解需求了，得想办法让它更懂你”。恰恰相反。形式方法那拨人求了工程师五十年“把规格写清楚”，没人理，因为摩擦受不了；现在来了个不知疲倦、毫不留情、把每句含糊都按字面执行的读者，你每写一句“加个搜索功能”，它当场把窟窿捅给你看。这是形式验证求而不得的规格强制力，以玩笑的方式到货了。评论区有人说得对：关键不是更好的提示词，是更好的委派，给完整任务、给明确的成功标准，审结果而不是逐行审。翻译过来就是：写规格。绕了五十七年，绕回 Hoare 的起点，只是这次读规格的东西不会累，也不会好心替你猜对。
再说那位 UnitBuilds。他后来在约束和模糊测试打底的前提下放权，五十万行的会计套件，四十来万行由 AI 生成，先有确定性护栏，再谈自主。模糊测试是 1988 年前后 Miller 在威斯康星带学生磨出来的老手艺；另一位读者建议的确定性结构检查，禁内部模块互导、禁弃用 API、禁循环依赖、违反分层就打回——这套东西 1979 年贝尔实验室的 Johnson 造过一回，叫 lint，出生原因就是 C 编译器不再替你查跨文件的事。我之前写包管理器那篇说过，同一组问题会在每个生态里被重新解一遍；验证这件事更狠，每个时代都以为自己发明了它。代码生产速度每甩开检查速度一个身位，答案的形状都一样：便宜的确定性规则打底，贵的人的判断花在刀刃上。lint 的幽灵每一代都在投胎。
有时候我会想：如果 1970 年代形式验证的成本能再低一个数量级，我们是不是早就习惯先写规格再写码，今天这轮坑根本不存在？反事实历史是廉价的，还是看实际怎么走的，业界用五十年投了“能跑就行、人肉兜底”，现在 AI 把人肉那部分抽走了，账单到期。
所以回到今天。有人喊下一代 CI 要“验证意图而不只是行为”，方向对，措辞我不太信，意图检查没有银弹，能落地的就是那两样老东西：确定性规则，加上独立来源的预期。真正变了的不是技术，是成本结构：意图验证从写代码的免费副产品，变成必须显式付钱的一道工序。先验证解决的是对的问题，再验证解决得对不对，这个顺序以前靠摩擦免费维持，现在得靠纪律花钱维持。工程判断力变得不可或缺，这话听着新，其实是把一笔暗账翻到了明面上。1968 年坐在加米施会议室里替你发愁待测工单的那拨人，要是看到今天流水线全绿、系统自我满足的样子，大概不会觉得陌生。认得出这个结构，焦虑能减一半；省下来的力气，拿去把那句“加个搜索功能”写成规格。
