当 AI 会写代码之后，软件还剩什么？

导语从一句AI 编程直接生成 C/汇编你怎么看出发我推演了一个完整闭环又亲手把它推翻了一半。这篇是复盘也是一份诚实的研究记录。前几天刷到一篇内容是说AI 编程直接生成 C 语言或者汇编语言你怎么看我的第一反应是看好。AI 写底层语言本质上是AI 原生低层软件工程高级语言会被降格成 AI 的中间表示IR——就像当年汇编被高级语言降格一样。这个问题往下挖会挖出一件比AI 会不会写代码重要得多的事。01 软件到底是什么一个被忽略的公式我们习惯把 Software 等同于 Code代码。但在 AI 时代这个等式得重写Software Intent意图 Specification规格 Constraints约束 Behavior行为 Verification验证Code 只是这个等式里最小的一块拼图。视角一变结论就出来了——AI 时代软件的核心资产正在从 Code 迁移到 Specification规格/规范。为什么因为代码可以由 AI 随时重新生成而系统到底要干什么、约束是什么、什么算对才是必须被人类长期持有、不能丢掉的东西。顺着这个判断有三个推论我认为才是这件事真正的精华推论一代码变成一次性产物Disposable Artifact。代码不再需要被精心呵护、长期维护它可以被丢弃、被重新生成。Spec 才是唯一需要长期保存的资产。推论二验证必须独立于生成。这是防作弊机制。AI 生成能力 ≠ AI 验证能力——你不能让出题、答题、判卷都是同一方。否则系统会完美地实现错误的目标后面会讲两个真实惨案。推论三人的稀缺能力从写代码上移到了定义正确性。未来最贵的人不是写代码最快的人而是能把什么是对的说清楚的人。02 它真的可行吗不能一刀切把spec 驱动当成万能银弹是错的。我按系统性质分了三层L1 技术原型完全可行。LLM 从结构化 spec 生成比从自然语言生成可靠得多——输入越结构化输出方差越小。验证层还有 40 年工具积累PBT、fuzzing、模型检查、证明助手可以直接用。L2 关键系统部分可行且有工业先例。AWS 用 TLA 设计 S3 / DynamoDB / EBS在规格层就发现了复制协议 bugseL4、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 上实现并共享同一套验证。32 项验证全绿。但比全绿本身更有教学价值的是三个发现第一C 未必更快。纯函数基线Python 56 ns/opC 却要 289 ns/op。为什么ctypes 跨语言边界的调用开销约 200ns吃掉了 C 的计算优势。结论很扎心抽象层越低不一定越好调用边界也是成本。第二验证通过 ≠ 验证在运行。最初 properties / differential 测试文件命名不符合 pytest 约定第一次跑出来12 passed其实漏跑了 9 项。验证完备性不是理论问题是这类小事一天天堆出来的。第三Hypothesis 的健康检查立了功。tmp_path 这个测试 fixture 在 100 个随机输入之间不重置前一组残留记录污染了下一组的幂等判断。框架在测试暴露错误之前就把问题拦住了——这是独立验证层价值的微观案例。05 最重要的结论Demo 只证明了一件很弱的事做到这里我停下来复盘得到一个让整个方向降温的结论。Demo 只能证明基于 SPEC 生成代码。而这件事本质上是传统软件工程本身。高级工程师读 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感兴趣,欢迎一起来深入交流。往期推荐《AI 编程代码生成与演进落地实践》一种可控的团队交付机制智谱 ZCode、DeepSeek dsh、Claude Code 横评看清楚再换,别被忽悠了