AI写代码越来越快，但写错的时候也越来越多。有没有一种办法，让AI在生成代码的那一刻，就"数学上不可能"违反你定下的规则？一门叫Bend的新编程语言，正在尝试这件事。
它的思路不是让AI更聪明，而是给AI套上一层"法律"和"证明"。Bend用"法律（Laws）"来精确表达人的意图，用"证明（Proofs）"来验证AI是否真的按意图实现了代码。同时，它还有一套高速编译器，保证执行速度不拖后腿。
速度：单核接近C，多核和GPU再翻百倍
Bend会编译成原生代码，单核运行速度接近C语言。如果动用16核或者GPU，执行速度可以接近单核的100倍。
在采用符号回归的基准测试中，Bend的成绩是：1核3.01秒，16核0.27秒，GPU0.53秒。这个数字放在传统语言的对比里，属于相当能打的水平。
编译速度同样夸张。Bend的类型检查器同时充当证明检查器，所以像Lean、Rocq这类语言要花几分钟编译的中等规模代码库，Bend能在1秒以内完成。
这意味着什么？AI代理改完源码后，可以立刻检查结果，不用等。
具体到数字：一个包含1万2800个定义的代码库，Isabelle和Agda要跑5分钟以上，Lean是36.2秒，Rocq是5.99秒，而Bend只要0.29秒。
不用写线程和锁，任务自动分到多核
并行处理是Bend的另一张牌。开发者不需要写线程、锁或者内核，就能把任务分散到多个核心上，由语言自己完成高效的并行执行。
对写惯了并发代码的人来说，这省掉的不只是几行代码，而是一整类容易出错的环节。
用"法律"锁死AI的越界行为
Bend最核心的设计，是让AI的代码生成变得可验证。
在LAWS.bend里声明的法律，会成为AI写代码时必须遵守的规则。Bend会让AI生成违反规则的代码这件事，在数学上变得不可能。
官方举了一个游戏的例子。假设你定义了一条"胜利不可能"的法则。之后你让AI加一个新功能："把棋盘绕一圈。"
如果没有法律约束，这个新功能合并进去，可能就把"胜利不可能"这条法则给推翻了。
而有了法律，Bend只允许那些能维持"胜利不可能"法则的代码改动通过。AI生成代码的可靠性，因此被大幅拉高。
装起来只要两步
想用Bend，门槛不高。先跑一遍官网提供的脚本完成安装，然后告诉AI代理去用Bend就行。
官方还建议在AGENTS.md里写上几条使用约定：
- 运行bend guide来学习它
- LAWS.bend保存重要规则
- 提交前运行bend PROOF.bend
- 尽可能把代码并行化
Bend被定位成一门有望推动"无bug的vibe coding"的语言。不过它自己也承认，目前还远未完成，欢迎使用者提交问题报告。
一门语言能不能真的把AI的错误挡在门外，最终要看有多少人愿意把规则写进LAWS.bend里。
热门跟贴