Bend：用数学证明阻挡AI代码错误
在AGI时代，人类或许不再直接编写代码，但仍需一种无歧义的方式向AI传达意图。Bend语言应运而生，它兼具C语言的速度与CUDA并行能力，更引入了Lean式的数学证明机制。通过LAWS.bend文件，开发者可以声明不可违背的规则，AI生成的任何代码若违反这些规则，将在编译阶段被直接拦截。这意味着合并一个Bug在数学上已不可能。Bend不仅让AI代理能即时验证代码正确性，还实现了从单核到GPU的自动并行加速，让开发者真正享受无Bug、高性能的编程体验。
在AGI经济时代，人类最终将停止编写和阅读代码，但我们仍需要一种无歧义的方式，告诉正在构建世界的AI们我们想要完成什么。
HN 评论区
308- LightMachine
你好，我是作者。
HN 工作人员：有人在我之前发帖了。能把标题改成
"Bend - 一种通过数学证明阻挡 AI 错误并能在 GPU 上运行的语言"吗？
各位：欢迎随时提问，但这次如果大家能稍微文明、尊重一点，我会非常感激。我在这上面投入了一年，几乎每天 16 小时，每周 7 天，而且我是免费开源的。你们完全可以用也可以不用。所以，如果能礼貌地指出偶尔的失败，而不是把我扔进熔岩坑，我会很感谢。
谢谢！
- mccoyb
在消化了大量关于其历史的内容后，我的理解是：
- 这个 Bend 跟旧版 Bend 没啥关系（除了名字）
- 这个 Bend 跟交互组合子（interaction combinators）也没什么关系
- 这个 Bend 是一个 QTT，它对亲和性（affinity）做了改动，从而强制保证了适合 GPU 的性能特性
- “在编译期的高阶”这个点很酷，让我想起了 Andras Kovacs 在 2ltt 和依赖类型语言中的分阶段（staging）工作
- 这个 Bend 很可能擅长“在代数数据类型（ADT）上的平衡递归计算”，并且可以并行化它们……但在稠密矩形数组计算上，可能不如 CUDA 或例如 Futhark
- 调度器的性能需要改进，或许能更好地处理平衡负载（看看 n 皇后问题和符号回归的数据）？
你打算如何处理不规则结构上的搜索或综合（SupaGen）？
- plastic041
这个项目的仓库有 2 万颗星，但只有 500 个 fork，issue 少于 300 个（包括已关闭的）。有点不对劲。
与其他编程语言相比：
- Gleam: 2.2 万颗星，1k 个 fork，3k 个 issue
- V: 3.8 万颗星，2.3k 个 fork，1.1 万 issue
- Ruby: 2.3 万颗星，5.6k 个 fork，1.9 万 issue
- Zig: 4.3 万颗星，3k 个 fork，1.4 万 issue
而且它仅仅在 4 个月内就获得了 1.6 万颗星。https://www.star-history.com/?repos=bendlang%2Fbend
此外，大家凭什么信任这个？我从未见过一种编程语言既没有 1) 更新日志 2) 下载旧版本的方式 3) 提交历史。
我不明白作者为什么觉得删除提交历史是个好主意。想象一下第一次看到这个项目：一个有 2 万颗星的仓库，却没有任何提交记录，issue 和 PR 也少得可疑。看起来不太正规。
---
我不太熟悉学术流程，但在我看来，仓库里一份由 Fable 撰写且未经评审的 PDF，算不上是一篇正经的“论文”。
- meghanto
必须说，自从 2023 年中关注 Taelin 的这个项目以来，当这门语言刚发布时，我没想到会迎来这样的反响。
很有趣的是，表面形式（cosmetics）往往主导了讨论，而 HN 的评论也奇怪地分裂成了两派：一派是轻蔑和怀疑的，另一派则对前者的反应感到难以置信和愤慨。
我原本期待的，是更多关于用例、基准测试、可能性、局限性（那些跟 git 历史无关的）以及未来开发范围的讨论。
- runeks
> 在通用人工智能（AGI）之后的经济中，人类最终将停止编写和阅读代码，但我们仍然需要一种无歧义的方式，来告诉构建我们周围世界的 AI 们我们想要做什么。
> 借助法律（laws），我们的意图可以比自然语言精确得多。
这难道不意味着代码现在就是“法律”了吗？也就是说，代码本身就是规范（spec）。
既然如此，有什么理由认为，为复杂系统编写这些“法律”会比编写实现它的传统代码更容易呢？
- svachalek
很酷的想法。我试着用它来移植一个我用 vibe coding 写的小会议安排 cron 任务，感觉挺契合的，因为它本质上就是在尝试满足我日历中的不变量（invariants）。
它基本上成功了，但 Claude (Opus 5) 确实有一些抱怨：
'基础库只包含一条算术定律：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 误解了什么。
- RomanKornev
> LAWS.bend
我喜欢“定律”这个想法，但我发现它们最终做的事情，往往是为了适应新功能而修改定律本身，这就本末倒置了。
这意味着某些定律需要被冻结。但又不能冻结所有定律，否则你就无法添加或修改任何东西。所以判断权仍然在人手中，我们又回到了“肉包”（meatbags，指人类）是瓶颈的局面。
我见过一些成功案例，在 CI 中添加这些类证明的检查，每当代理（agents）做出非理性行为时触发。我绝对认为这应该是每个代码库的一部分。
还有一个 https://code-contracts.cc/，它将代码和证明放在一起。
- djaro
我对网站演示的主要体验是：我让它添加一个简单的功能，这甚至不一定能让你赢下游戏，结果它在一个“定律被破坏”的循环中消耗了超过 10 万 token，直到可能添加成功，也可能没有。在仅仅为了加一行墙（让向上传送两格不能获胜）就烧掉了五十万 token 后，我的 API key 触发了速率限制，从而中断了这个循环。
此外，解决方案感觉像是拼凑出来的。我让它让空格键水平翻转棋盘，结果它把整个棋盘做得完全对称，包括两根旗杆。到了某个节点，它要么得说“在不破坏定律的情况下这不可能”，要么想出一个真正的变通办法，因为如果我在做游戏，突然出现两个终点对我来说就是 unwanted behavior（不想要的行为）。
- mpweiher
> 人类最终将停止编写和阅读代码，
“由于 FORTRAN 应该几乎消除编码和调试……” —— FORTRAN 报告，1954
http://www.softwarepreservation.org/projects/FORTRAN/BackusE...
- tyushk
Victor Taelin 的工作（HVM）让我对交互组合子（interaction combinators）作为编译目标产生了兴趣。我现在正在作为大学研究的一部分实现它。很高兴看到 Bend 2.0 发布！