导语：从一句"AI 编程直接生成 C/汇编你怎么看"出发，我推演了一个完整闭环，又亲手把它推翻了一半。这篇是复盘，也是一份诚实的研究记录。
前几天刷到一篇内容是说：AI 编程直接生成 C 语言或者汇编语言，你怎么看？我的第一反应是：看好。AI 写底层语言，本质上是"AI 原生低层软件工程"，高级语言会被降格成 AI 的中间表示（IR）——就像当年汇编被高级语言降格一样。这个问题往下挖，会挖出一件比"AI 会不会写代码"重要得多的事。01 软件到底是什么？一个被忽略的公式
我们习惯把 Software 等同于 Code（代码）。但在 AI 时代，这个等式得重写：Software = Intent（意图）+ Specification（规格）+ Constraints（约束）+ Behavior（行为）+ Verification（验证）
视角一变，结论就出来了——AI 时代，软件的核心资产正在从 Code 迁移到 Specification（规格/规范）。为什么？因为代码可以由 AI 随时重新生成，而"系统到底要干什么、约束是什么、什么算对"，才是必须被人类长期持有、不能丢掉的东西。顺着这个判断，有三个推论，我认为才是这件事真正的精华：推论一：代码变成"一次性产物"（Disposable Artifact）。代码不再需要被精心呵护、长期维护，它可以被丢弃、被重新生成。Spec 才是唯一需要长期保存的资产。推论二：验证必须独立于生成。这是防作弊机制。"AI 生成能力 ≠ AI 验证能力"——你不能让出题、答题、判卷都是同一方。否则系统会"完美地实现错误的目标"（后面会讲两个真实惨案）。推论三：人的稀缺能力，从"写代码"上移到了"定义正确性"。未来最贵的人，不是写代码最快的人，而是能把"什么是对的"说清楚的人。02 它真的可行吗？不能一刀切
把"spec 驱动"当成万能银弹是错的。我按系统性质分了三层：- L1 技术原型：完全可行。LLM 从结构化 spec 生成，比从自然语言生成可靠得多——输入越结构化，输出方差越小。验证层还有 40 年工具积累（PBT、fuzzing、模型检查、证明助手）可以直接用。
- L2 关键系统：部分可行，且有工业先例。AWS 用 TLA+ 设计 S3 / DynamoDB / EBS，在规格层就发现了复制协议 bug；seL4、CompCert 证明了"窄而深"的路线能走通。AI 的增量价值，是把"spec → code"的成本打下来——这恰恰是传统形式化方法最缺的一环。
- L3 普适软件工程范式：不可行，也不该追求。判据只有一条：这个系统的"错误"，能被形式化定义吗？
UI 好不好看、文案通不通顺，这类"错误"没法形式化，也就没法放进 spec 驱动里。别强求。03 最难的问题：Spec 自己也会烂
Spec 也会出 bug。而且Spec 的 bug 比代码 bug 贵得多——因为系统会"完美地实现错误的目标"。- Ariane 5 火箭：复用旧系统的隐含约束在迁移中丢失，火箭升空 37 秒后自毁。
- Mars Climate Orbiter 火星探测器：一边用公制、一边用英制，单位不一致，探测器坠毁。
这两起事故，都不是代码写错了，是 spec（规格/接口约定）层失败了。我的解法方向是：选择性形式化 + 多实现差分检验（行为一旦分歧，就是 spec 缺陷的探测器）+ spec 审批门禁。生成可以是概率的，接受必须是确定的。每一个环节，都由独立于生成方的机制来监督。
本质是把系统做成"对抗性分工"——生成方和验证方利益不一致，才能互相暴露问题。04 我真的写了一个 Demo
光说没用，我做了个最小闭环 inventory-demo：一个库存扣减服务，用同一份 Spec，分别在 Python 和 C 上实现，并共享同一套验证。第一，C 未必更快。纯函数基线：Python 56 ns/op，C 却要 289 ns/op。为什么？ctypes 跨语言边界的调用开销（约 200ns）吃掉了 C 的计算优势。结论很扎心：抽象层越低，不一定越好，调用边界也是成本。第二，"验证通过" ≠ "验证在运行"。最初 properties / differential 测试文件命名不符合 pytest 约定，第一次跑出来"12 passed"，其实漏跑了 9 项。验证完备性不是理论问题，是这类小事一天天堆出来的。第三，Hypothesis 的健康检查立了功。tmp_path 这个测试 fixture 在 100 个随机输入之间不重置，前一组残留记录污染了下一组的幂等判断。框架在测试暴露错误之前就把问题拦住了——这是"独立验证层价值"的微观案例。05 最重要的结论：Demo 只证明了一件很弱的事
做到这里，我停下来复盘，得到一个让整个方向"降温"的结论。而这件事，本质上是传统软件工程本身。高级工程师读 PRD 写实现，从来如此。如果"spec 驱动"只是"写好文档再让 AI 写代码"，它只是工作流改进，不是范式转移。- 错误注入（最致命）：所有实现一次写对，验证从没抓过一次错。"全绿"在证据上等价于空转。缺 mutation testing——故意生成违反 spec 的实现，验证套件检出率必须 100%，才能说"验证有牙齿"。
- 替换实验：只有静态两套实现，没有"运行中系统换语言"的动作。替换成本，才是"实现可替换"这个命题的真正内容。
- 演进实验：spec 只变过一次，没测过需求变更怎么传导到实现和验证。
- 生成-修正闭环：从未发生。"AI 修正实现"这条循环，才是"AI Software Engineering"区别于"AI 写代码"的唯一分界线。
这个方向的核心承诺，恰恰是 demo 天生证明不了的部分。真正值钱的不是"生成"（生成最便宜），而是：验证有牙齿、替换廉价、演进可控——三者都需要时间尺度或对抗性实验。还有一个同源性盲区：如果 spec、实现、验证都出自同一个认知主体，结构分离 ≠ 认知独立。真正的独立性，需要对抗方。06 方法论修正：把 Demo 设计成"证伪"，不是"证成"
Demo 应该设计成证伪实验，而不是证成实验。
"证明能跑通"的证成 demo，证据价值趋近于零；"证明它在哪里失败、验证能不能抓住坏实现"的证伪实验，才是这个方向真正的证据链。所以我下一步最高优先级的事，是做错误注入：生成至少 10 个故意违反 spec 的实现（负库存、幂等失效、失败改库存、并发超卖……），要求验证套件 100% 检出。这一关过了，这个方向才从"文档驱动的新名字"，升级成"有牙齿的正确性保证"。07 一句话收尾
AI Coding 的终局，不是"AI 帮程序员写代码"，而是"人定义系统目标与约束，AI 寻找从意图到机器执行的最优实现"。但这个判断成不成立，取决于验证体系有没有牙齿，而不是生成能力有多强。证明"能生成"很容易，证明"值得这么生成"才是研究本身。
- 代码正在变成可丢弃的产物，Spec 才是长期资产。
- 验证必须独立于生成——出题、答题、判卷不能是同一方。
- 别急着庆祝"跑通了"，先问一句：你的验证，真的咬得住坏实现吗？
如果这篇文章让你对这个方向多了一份清醒，欢迎转发给也在用 AI 写代码的朋友。如果你对这个Demo感兴趣,欢迎一起来深入交流。
夜雨聆风