Bend：用数学证明阻挡AI代码错误

▲ 454nicolas-siplis212 HN 评论区

在AGI时代，人类或许不再直接编写代码，但仍需一种无歧义的方式向AI传达意图。Bend语言应运而生，它兼具C语言的速度与CUDA并行能力，更引入了Lean式的数学证明机制。通过LAWS.bend文件，开发者可以声明不可违背的规则，AI生成的任何代码若违反这些规则，将在编译阶段被直接拦截。这意味着合并一个Bug在数学上已不可能。Bend不仅让AI代理能即时验证代码正确性，还实现了从单核到GPU的自动并行加速，让开发者真正享受无Bug、高性能的编程体验。

在AGI经济时代，人类最终将停止编写和阅读代码，但我们仍需要一种无歧义的方式，告诉正在构建世界的AI们我们想要完成什么。
阅读原文 →HN 评论区RSS

HN 评论区

212
  1. LightMachine

    大家好，我是作者。

    HN 工作人员：有人在我之前发帖了。能否将标题改为

    "Bend - 一种通过形式化证明来阻断 AI 错误并在 GPU 上运行的语言"？

    各位：欢迎提问，但这次如果各位能稍微文明、尊重一点，我将不胜感激。我为此项目投入了一年，每周 7 天，每天近 16 小时，并且是免费开源的。你们大可以不用它。所以，如果能礼貌地指出偶尔的失败，而不是把我扔进熔岩坑，我会非常感激。

    谢谢！

  2. mccoyb

    在我大量阅读了相关历史内容后，我的理解如下：

    - 这个 Bend 与旧版 Bend 其实没有实质关系（仅名字相同）

    - 这个 Bend 与交互组合子（interaction combinators）也没什么关系

    - 这个 Bend 是一种 QTT（量子张量树），它对亲和性（affinity）做了修改，以强制实现适合 GPU 的良好性能特性

    - “在编译时的高阶能力”很酷，让我想起了 Andras Kovacs 在依赖类型语言中关于 2ltt 和分阶段（staging）的工作

    - 这个 Bend 可能擅长“在代数数据类型（ADT）上进行平衡递归计算”，并能进行并行化……但在密集矩形数组计算方面，可能不如 CUDA 或 Futhark

    - 调度器（scheduler）的性能需要改进，以可能更好地处理平衡负载（看 n 皇后问题和符号回归的数据）？

    你们打算如何处理针对不规则结构的搜索或合成（SupaGen）？

  3. meghanto

    不得不说，自从 2023 年中一直关注 Taelin 的这个项目，当这门语言刚发布时，我完全没想到会收到这样的回应。

    很有趣的一点是，表面形式（cosmetics）往往主导了讨论，而 HN 的评论也奇怪地分裂成两派：一派非常轻蔑或怀疑，另一派则对前者的反应感到难以置信和愤慨。

    我原本期望看到的是更多关于用例、基准测试、可能性、局限性（且这些局限性不应是关于 git 历史的）以及未来开发范围的深入讨论。

  4. plastic041

    这个项目的仓库有 2 万颗星，却只有 500 次 fork，issue 总数（含已关闭）不到 300 个。有些不对劲。

    与其他编程语言相比：

    - Gleam: 2.2 万颗星，1000 次 fork，3000 个 issue

    - V: 3.8 万颗星，2300 次 fork，1.1 万 issue

    - Ruby: 2.3 万颗星，5600 次 fork，1.9 万 issue

    - Zig: 4.3 万颗星，3000 次 fork，1.4 万 issue

    而且它仅在 4 个月内就获得了 1.6 万颗星。https://www.star-history.com/?repos=bendlang%2Fbend

    此外，人们该如何信任这个项目？我从未见过一门编程语言没有 1) 变更日志 2) 下载旧版本的方法 3) 提交历史。

    我不明白作者为什么认为删除提交历史是个好主意。想象一下第一次看到这个项目：一个有 2 万颗星的仓库，却没有提交记录，issue 和 PR 也少得可疑。这看起来很不正规。

    ---

    我不太熟悉学术流程，但在我看来，仓库里一份由 Fable 撰写且未经评审的 PDF，算不上正式的“论文”。

  5. svachalek

    很酷的想法。我试着用它来移植一个我用 vibe coding 写的小会议安排 cron 任务，感觉非常契合，因为它本质上是在尝试满足我日历中的不变量（invariants）。

    基本上成功了，但 Claude (Opus 5) 确实有一些抱怨：

    'Base 只内置了一条算术定律：U32.add_comm。没有序理论。PROOF.bend 的 163 行代码中，约有 60 行是 cmp_refl, and_false, and_comm, le_max_l, le_max_r, add_succ——这些是你本该假设存在的引理。你本该每个项目写一次就再也不用写了，但得为此预留预算。'

    'Base 的 Nat.max 在证明中无法使用。它是 Bool.pick(Nat, Nat.is_lt(a,b), b, a)，而证明无法对计算值进行模式匹配。我写了一个结构递归的 nat_max，以便它能与 Nat.cmp 同步展开。'

    '我最想要的定律是：“没有两个输出计划重叠”。我没能陈述它。这需要 collapse 输入已排序作为假设，而 Base 的 List.sort 没有提供排序定律——因此要达到这一点，意味着必须先证明归并排序的正确性。这才是衡量“原则上可证”与“今天下午就能证出”之间差距的诚实标准。'

    我基本上辅修过 CS，所以在证明方面我是个菜鸟。我不确定这是有价值的反馈，还是仅仅是 Claude 误解了什么。

  6. RomanKornev

    > LAWS.bend

    我喜欢“定律”这个想法，但我发现它们最终的做法往往是：为了适应正在开发的新功能而直接修改定律本身，这就违背了初衷。

    这意味着某些定律需要被冻结。但不能冻结所有定律，否则你就无法添加或修改任何东西。所以判断权依然在人手中，我们又回到了“肉包（meatbags，指人类）”是瓶颈的局面。

    我见过一些成功案例，即在 CI 中添加这些类证明检查，每当 Agent 做出不合理操作时触发。我绝对认为这应该是每个代码库的一部分。

    还有 https://code-contracts.cc/，它将代码和证明放在一起。

  7. garrisonj

    问题在于，我得靠 vibe coding 来编写所有定律，而且这些定律可能是错的。

  8. tyushk

    Victor Taelin 的工作（HVM）让我对将交互组合子（interaction combinators）作为编译目标产生了兴趣。我现在正在作为大学研究的一部分实现它。看到 Bend 2.0 发布真是太酷了！

同日更多故事

2026-09-17