bendlang/bend

解决什么问题

当 AI 承担越来越多编码工作，瓶颈就从写代码转移到了审代码。测试只能覆盖你想得到的例子，覆盖不了你忘掉的约束。Bend 的做法是把约束本身变成构建的一部分：在 LAWS.bend 里声明规则，任何人（包括 AI）改动代码，编译器都要求给出这些规则仍然成立的数学证明，否则拒绝通过。README 里的演示很具体：一个「不可能获胜」的游戏，当 Agent 被要求加上边界穿越功能时，它只能选择加一堵墙，而不是把 bug 合并进去。

有什么不同

常见的验证方案是外挂式的：Lean、Agda 这类证明助手，或者给主流语言加精化类型层，验证器和运行时往往是两套东西，证明检查器也慢。Bend 把依类型、纯函数、线性值和并行运行时放进同一门语言，被证明的代码就是编译到 C、CUDA、Metal 或 JavaScript 的那份代码。真正突出的只有两点：检查器速度（声称亚秒级，而其他助手常以分钟计）和分治式并行（无需线程、锁或手写 kernel，递归拆分后自动铺到 CPU 核或 GPU 上）。相对普通测试，law 是全称量化的而非抽样；相对 Lean，代价是生态小得多、几乎没有 tactic。

适合谁

适合已经在用编码 Agent、且业务规则严格（游戏逻辑、账本、状态机）的团队——一旦不变量被破坏代价很高，又不想逐行 review diff。也适合对带仿射的依类型论和快速检查器感兴趣的研究者。如果你今天就要一门生产语言，请绕开：标准库没有 TLS、HTTP、JSON 和 regex，不支持 Windows，Base 很小，没有 tactic，证明只能手写。

上手成本

安装是一条 curl 管道脚本。README 自己提醒：安装版 bend 会忽略项目里的配置文件，而从 checkout 跑 bun bend2/main.ts 会读取它们，检查不可信代码时要注意这个差别。需要 clang 14+，使用 ! 并行算子则需要 clang 19+ 或 CUDA 12。限制清单异常坦诚也异常长：全部需要标注、没有类型类和宏、值具有仿射性不能共享、字符串是链表、每个程序只生成一个 C 文件且没有增量编译、原生编译很慢建议开发期用 JS 目标。编译器 99% 由 AI 编写且尚未完全审计；检查器本身没有证明，只有 --verdict 依赖经过 Lean 形式化的内核。这是重写的 Bend 2，Bend 1 的程序和 HVM 都不能沿用。

点评

项目 2023 年就存在，积累了约 2.4 万 star，但热榜记录只有两天、每天约 +110，更像细水长流而非爆发；Hacker News 上「Bend 2 Is Here」只有 18 分，说明关注面仍偏小众。把 law 做成带证明、可强制执行的 AGENTS.md，在 Agent 写代码的时代确实问对了问题，而且项目对缺陷的坦白程度罕见。作为日常生产力工具它还远远不够格；作为「可验证的 AI 辅助开发」实验，它值得持续观察。建议先找一个证明密集的小 demo 试水，再考虑用在真正重要的代码上。