把团队规矩写成定理：这门语言说，AI 违规的代码在数学上进不了主干

凌晨三点，coding agent 跑完了一个八小时的长任务。测试全绿，diff 干净，CI 冲你笑。可团队有条从没写进测试的规矩——用户余额不允许为负——被它绕过去了。没有人说谎，没有人失职，坏事照样发生。

9 月 17 日，Hacker News 上一篇帖子攒了两百六十多个赞，讲的就是这个场景的一剂解药。语言叫 Bend，官网标语直译过来是：一门用证明拦住 AI 错误的快速语言。作者 Victor Taelin，就是这个圈子里的老熟人，2024 年 5 月他那版"跑在 GPU 上的语言"在 HN 拿过一千多个赞。这次的 Bend 2 是推倒重来的新语言，README 里写得明白：Bend 1 的程序带不过来，HVM 运行时也重写了。

新东西怎么用？三个文件。LAWS.bend 里写团队的不变量，比如"任何移动都不能穿过墙"；AI 写完代码，再在 PROOF.bend 里写出符合这些定律的证明；提交前跑一下检查器，一秒之内给你判决。过不了，AI 自己重试，直到证明成立或者放弃。README 里有一句大实话：LAWS.bend，就是背靠证明的 AGENTS.md。散文变成了定理，自觉变成了数学。

底层是一门叫 BendTT 的仿射依赖类型论。类型检查器就是证明检查器，和 Lean、Rocq 同宗。线性类型把运行时闭包整个禁掉，罗素悖论、Girard 悖论这类能炸穿类型系统的东西，在语言层面就没入口。代价也摆在明面上：没有 tactics，没有证明搜索，没有类型推断——全拿来换检查速度了。Lean 和 Rocq 核一份证明要分钟级，Bend 把它压到一秒上下。这个差距对人是琐事，对 AI 是工作流：每次改动都能当场重验，验证从"交卷后阅卷"变成了"边写边判"。

单文件同时是 CPU 程序和 GPU kernel，编译到 C，再由宏分发到 Metal 和 CUDA。官方口径是单核接近 C，GPU 比单核快上百倍。递归必须有界，程序必然终止，无限路径用归纳法收口——想关掉这层保护也有门：显式挂上 unsafe 标记，自己签字画押。HN 上作者的演示词说得更大胆：在定律覆盖到位的前提下，合并一个 bug 在数学上不可能。

小字比正文精彩，展开三行。

第一行，演示里就露了馅。有人当场合上检票员的面拆墙——AI 把直线路径改成了对角线绕行，一步跨过被移除的墙，定律字面上没违反，意图上已经跑路。写帖人的原话值得抄在这里：写法律本身，成了比写代码更大的问题。Taelin 的回应也诚实：定律只保护你想得起来写的那部分，这不是银弹。他补了一个正经用例——一句"所有账户余额总和为零"，就能把 The DAO 那类重入漏洞挡在门外。

第二行，定律自己谁写？评论区问得直接：定律也是 vibecode 出来的，写错了怎么办。作者回了一个字：true。还有实践者用 Claude Opus 5 真移植了一个小工具，能跑，但标准库薄得可怜，一百六十三行证明里六十行是自己手搓的基础引理。作者的愿望清单上写着：需要一套 mathlib。

第三行，仓库本身是个行为艺术。整个 git 历史被压成一个 commit，署名 Bend 2.0.5，合作者一栏写着 Claude Fable 5.1。压掉历史的理由写得坦白：清掉个人信息、AI 生成的残渣，还有一段专有代码。社区当场开骂——有人指出 force-push 清不掉任何东西，历史都躺在 fork 和缓存里，毁了的是信任本身；作者松口，说可以恢复一份脱敏的历史。性能图全是动图，没有数据表，百倍加速只能先当口号听。现状清单倒是诚实得过分：没有 Windows，没有 64 位浮点，字符串是链表，没有 HTTP 库、没有 JSON、没有调试器、没有 LSP。README 还自曝编译器九成九是 AI 写的、没做过完整审计。商业模式倒清晰：编译器开源，配套的 Bender 证明 agent 收钱，众筹平台上已经出现了对应的融资页。

把这三行小字叠回正文，这事还值不值得看？值得。编程 agent 把产能问题解决到七成之后，瓶颈正在挪窝——挪到"怎么把意图说清楚"。AI 已经会写证明，会写代码，甚至写了这个编译器自己。剩下给人的活儿，是决定哪些规矩值得立成法。这个活儿机器替不了，因为它本质上是在回答：你要的到底是什么。

你的项目里，那些没写进测试的"用户余额不许为负"，还剩几条？