Bend 让 agent 自己证明它没破坏你的规矩

Bend 自称是一门"用证明拦住 AI 犯错的快速语言"，听上去像三个不相干的卖点硬钉在一起，直到你看清它怎么运作。官网 https://bend-lang.com/ ，源码在 github.com/bendlang/bend，一夜之间在 Hacker News 拿了 139 分。

机制一句话说得清。你把你的不变量写进一个叫 LAWS.bend 的文件：那些永远不能被破坏的性质，用形式化的方式写出来。代码合并之前，agent 必须跑 bend PROOF.bend，生成一份机器可校验的、Lean 风格的证明，说明它的改动没有违反这些不变量。他们的演示是一个游戏，法条写着"赢是不可能的"，于是系统拒绝任何会破坏这条已证明不变量的实现改动。不是标记。不是警告。是拒绝，因为证明闭合不了。

这是"强制优于叮嘱"这个论点目前能找到的最纯粹形态，而这个论点整个月都在攒证据。你没法在 system prompt 里写一句"绝不要破坏这个不变量"然后当真，因为 prompt 是请求，证明义务是墙。有意思的设计后果在评审环节：不再是一个人读 diff、努力想象它可能会弄坏什么，而是机器要么给出证明要么给不出，人的工作往上挪一层，变成决定哪些法条才是对的法条。你对问题的理解成了产物。代码反而变成可以商量的部分。

另一半是性能，也是它不只是个验证玩具的原因。Bend 声称 C 级速度，编译到一个并行运行时，同一个二进制文件能跨 CPU 核心或 GPU kernel 跑，不用谁手写 kernel 代码或管线程。携带证明的代码历来是吞吐量的坟场，所以把这种保证和 CUDA 级并行绑在一起，是让它值得一试的那个赌注。

该降温的地方也要说。项目直说自己还在演进、预期有 bug，页面上没有版本号也没有明确的许可证，背后没有具名组织，只有一个仓库和一个 Discord。整个想法底下还压着一个非常硬的未解问题：谁来验证 LAWS.bend 写的就是你真正想说的意思。证明的质量上限就是法条的质量，而写出正确的形式化规格，恰恰是四十年来把无数人打败的那一部分。