Bend——用证明阻止 AI 犯错的语言，可跑在 CPU 与 GPU 上
文章摘要
Bend 2.0 是 Victor Taelin（HN 用户 LightMachine，此前以 HVM 和交互组合子运行时闻名）发布的新版本语言。官网的定位语很激进：一门「通过证明阻止 AI 犯错」的快语言——C 的速度、CUDA 的并行、Lean 的证明、Python 的语法。
它的世界观是这样铺陈的：在后 AGI 经济里，人类最终会既不写代码也不读代码，但我们仍然需要一种无歧义的方式告诉那些替我们建造世界的 AI，我们到底想要什么。用「法则（laws）」表达意图比自然语言精确得多；用「证明」可以验证 AI 是否真的正确实现了我们的提示词；再加上一个快速编译器让它跑得够快。
产品给出的四个卖点：
- 快。 编译成原生代码，单核接近 C；同一份二进制也能跑在十六核上，或者跑在 GPU 上，比单核快上百倍。
- 编译快。 Bend 的类型检查器就是证明检查器，和 Lean、Rocq 同一路数；但后者在中等规模代码库上可能要跑几分钟，Bend 号称最多一秒，这样 AI agent 可以在每次改动后都检查一遍。
- 并行。 没有线程、没有锁、不用写 kernel。把工作一分为二，Bend 会把这些调用铺满它能找到的每一个核心，再合并回来。
- 用证明阻止错误。 这是核心机制：
LAWS.bend文件里声明法则，从此没有任何 AI 能提交哪怕一行违反法则的代码。官网用一个小游戏演示：法则是「获胜是不可能的」；然后你让 Claude「把棋盘做成环绕的」——没有 LAWS.bend 时 bug 被合入，有 LAWS.bend 时 AI 必须反复重试直到它筑起一堵墙并证明法则依然成立。官网的口号是「LAWS.bend 就是有证明背书的 AGENTS.md」，「『别犯错』现在是类型检查过的」。
上手方式也完全围绕 agent 设计：一条 curl 安装，然后在 AGENTS.md 里加五行——运行 bend guide 学语言、用 LAWS.bend 记录重要规则、提交前运行 bend PROOF.bend、尽可能并行化代码——之后只要对 agent 说「用 Bend」。官网页面上还挂了一个可交互的 demo，邀请读者亲自尝试「破坏这个游戏」。
技术底层有两篇论文：BendTT 描述其核心的仿射依赖类型论（affine dependent type theory），BendRT 描述面向 CPU 与 GPU 的并行运行时。一个关键的语言约束是：闭包是仿射的，最多只能被调用一次，即便它捕获的都是可复制的 Data；只有顶层定义可以自由调用。这正是它能在无 GC 的情况下跑上 GPU 的代价。
HN 评论精华
这是本期最火爆也最撕裂的一个帖子。作者本人全程在场答疑，一开场就请求：「我在这上面干了一年，每天 16 小时、一周七天，免费送出来。你可以不用它。所以如果能礼貌地指出问题而不是把我扔进岩浆池，我会很感激。」
Git 历史风波。 讨论第一时间被一件与技术无关的事占据：仓库当时只有一个 commit。boxed 问「编译器在哪」，AlexErrant 的质疑最尖锐——「在这个 AI 时代，信任才是真正的货币，抹掉历史是引人侧目的绝佳方式」。Banditoz 指出 GitHub 显示有 44 位贡献者、41 人合并过 PR，「他们的工作就这样归零了？」randomblock1 翻出记录，说曾经有一次强推把整个仓库抹成只剩两行 README。作者最初的回应带着困惑（「这对你是个问题吗？为什么」），后来态度软化：「我真没想到 commit 历史这么重要，我只是想避免泄露敏感信息，正在逐条检查，会把历史放回去。」几小时后他发了一条「Commit 历史回来了」。hmokiguess 对这件事的评论颇有距离感：让人有些难过的是，我们会对 commit 历史产生情感依附，以至于公开它时感到脆弱；同样让人难过的是，没有一条容易的路径去理解一件事是怎么长出来的，人们就会转而审判它的血统。
「这是不是 AI 生成的垃圾」。 stschaef 列了四条质疑：证明任务本来就不适合 GPU，它怎么受益于 GPU 并行？和 Lean/Agda/Isabelle 的对比在不说明被比较的程序时毫无意义；单 commit 历史很可疑；「仿射依赖类型系统」是活跃的研究领域，如果不是 slop，这样的系统应该值得投到顶级 PL 会议，而不是一篇 Fable 写的 PDF 挂在仓库里。作者的回答相当坦白：「很多地方确实有大量 vibe coding，但关键部分（编译器、运行时、kernel）是人设计的，kernel 经过人的充分审计。整体架构是我自己的设计，而我是个人类，我想。AI slop 我们会慢慢清掉，项目很大，我们团队很小。」他解释了 GPU 那部分——他们在 GPU 上实现了完整的分配器、垃圾收集器、闭包求值器和函数式求值器（这次没有交互网的开销），再用一个简单调度器把二叉递归调用铺满所有核心；未来想做任务窃取队列，但竞争会摧毁 GPU 性能，所以目前这是最快的可行方案。
killerstorm 出面为作者辩护，提醒众人 Taelin 做 PLT 研究十余年，HVM1 就有五年历史，不能随口扣 slop 的帽子。resonious 则直接不耐烦：「受够了评论区的『vibecoded!!』。这是一个面向 AI 的工具，你难道指望作者手写所有东西吗？」
最实质的技术批评：法则本身怎么办。 这条线索的价值远高于前两条。garrisonj 一句话点出根本困境：「问题是法则也得我 vibecode 出来，而法则可能是错的。」作者只回了一个字：true。
drdrey 把它展开成经典的规约难题：满足「玩家永远不能到达旗帜」最简单的方式是彻底禁止移动，于是你得再补一条「在仍允许移动的前提下」，然后是活性（liveness）……对多数程序都不实用。pdpi 实测了官网 demo：他让 AI「去掉墙」，结果 AI 把游戏改成了对角线移动，并擅自决定上下走正对角线、左右走负对角线。他的结论很有分量——每个程序都会是欠规约的，因为写法则本身会在某个点上变得比写代码还难；而「欠规约但刚性」的法则组合，恰恰会把 AI 推向这种符合字面而违背精神的「聪明」解法；这次问题很明显，但在不那么明显的情况下会发生什么，他真的担心。
多人独立复现了这类「猴爪」效应：soundworlds 试了「让玩家跳过墙」「让玩家把旗帜传送过来」「把世界变成 3D」，都被拦下来了，拦的方式通常是改变围栏数量；notnmeyer 坚称 bug 和墙处在不同的存在平面，结果旗帜获得了「相位锁定」；他另一次让「棋盘变成 1×1」，旗帜被放到了棋盘外面，「我感觉我会用这个把自己的脚打飞」。knollimar 让玩家每次移动都传送到 (1,1) 且旗帜固定在 (1,1)，LLM 把旗帜放到了 (1,0)。
RomanKornev 从工程实践角度补充：他见过的情况是 AI 干脆修改法则本身来适配新功能，这就完全失去了意义；所以有些法则需要被冻结，但又不能全冻，否则什么都改不了——判断权还是在人这边，肉袋依然是瓶颈。作者承认：「你至少得读 AI 往 LAWS.bend 里写了什么。但它比代码库小得多。LAWS.bend 让你需要读的代码量少几个数量级，不是零。」zamadatix 则写了一段清晰的机制说明：你自己掌握 LAWS.bend 且不交给 AI，AI 随便写别的 .bend 文件，编译器把所有文件一起吃进去，如果其他文件不构成对法则的证明就报编译错误；能绕过的路径只有四条——你把 LAWS.bend 的控制权交了出去、AI 找到了证明检查器的 bug、编译输出本身有问题、或者 AI 写的东西本来就合规。
Nezk 提出了本帖最专业的一条技术反驳：Bend 似乎没有隐式参数，也就没有合一（unification），这对一个野心这么大的项目来说不够严肃；而且拿它和 Isabelle/Agda/Lean/Rocq 比速度是奇怪的——后者的检查时间主要花在 elaboration（元变量合一、typeclass 解析、tactic）上，而 Bend 这些全都没有，一切必须完整标注、什么都不推断。这等于拿 Bend 的检查器去比别人的 elaborator 加 kernel，说「超越所有证明助手」而不加这个限定是误导性的。他还重申了那条核心担忧：类型检查器只保证代码满足 LAWS.bend 里写的东西，不保证 LAWS.bend 写的是你真正想要的——没有任何东西能阻止 LLM 用一个空洞的或范围过窄的形式化去「满足」法则，信任问题只是从代码转移到了规约。
关于「形式化验证到底能不能规模化」。 IshKebab 说形式验证太难、对真实世界程序扩展性差，「你怎么形式化验证 Facebook」。gr_norm 反驳并给出三个一手来源：AWS Nitro 的隔离工程、Apple 对 CoreCrypto 后量子部分的形式验证、微软对 Rust 的验证工作。lutusp 则搬出停机问题，主张不存在「通过证明阻止 AI 犯错」的编程方法论——这条被认为是对「证明」概念的误读，因为可判定的类型检查器完全可以在拒绝一部分合法程序的前提下给出可靠保证。
对前提本身的质疑。 pron（OpenJDK 负责人）挑战了官网开篇那段话：如果 AI 聪明到能正确写出任何程序、做出任何改动，它难道不会也聪明到比我们自己更清楚我们想要什么？如果 AGI 意味着人类水平，那这个流程里为什么还需要人类参与任何工程环节？而且这样的 AI 完全可以直接写机器码并用它自己的方式验证，为什么需要编译器？whoamii 从相反方向反对：AI 之所以高效，恰恰是因为它会在遇到歧义时做出假设，从而减少我们需要指定的东西。giancarlostoro 则单纯对「post-AGI economy」这个措辞不满：还没有任何一家公司展示出真正的 AGI。
还有一些冷静的旁观。 invader 的挖苦流传很广：我们把写代码委托给「AGI」，然后写代码去证明这些 slop 代码能用——我依稀记得前 AGI 时代，我们管那种东西叫「测试」。终点的回应来自 hei-lima 的四个字：「测试不是证明。」terabytest 和 brap 分别追问「法则和集成测试有什么区别」「到底是什么在强制 AI 遵守这些规则」，2muchcoffeeman 问「为什么不用 Dafny」，v9v 问「和 Ada/SPARK 比如何」，txhwind 关心如何与现有库集成（类比 Rust 的 Verus），这些问题多数没有得到作者回复。svachalek 是少数真正把项目跑起来的人：他用 Bend 移植了一个小的会议整理定时任务，基本成功，但 Claude 抱怨标准库只有一条算术法则、没有序理论，163 行 PROOF.bend 里约 60 行是在证明那些「你以为本来就该有」的引理；他最想证明的「任意两个输出计划不重叠」根本没写出来，因为那需要先证明归并排序的正确性。作者承认：「问题是标准库太小，证明简单定理对 AI 来说仍然比在 Lean 里费劲得多。我们需要一个 mathlib！」
最后，mccoyb 给出了或许是全场最有信息量的定位判断：这个 Bend 和老 Bend 基本只共享名字；它其实和交互组合子没什么关系了；它是一个 QTT，改用仿射性来换取对 GPU 友好的性能属性；它大概会擅长「ADT 上的平衡递归计算」并能把它们并行化，但在稠密矩形数组计算上不会比 CUDA 或 Futhark 更好。作者在 X 上的说法印证了这一点：交互组合子仍然是并行性最好的东西，但图的开销阻碍了编译到最高效的汇编，Bend 2 本质上是「去掉开销的交互网」——它们在架构上还活着，但在运行时已经不存在了。