Bend：一种通过证明拦截 AI 错误并在 GPU 上运行的语言
Hacker News 摘要原标题：Bend – A language that blocks AI mistakes via proof and runs on GPUs
Bend 是一种兼具 C 语言运行速度、CUDA 并行能力以及 Lean 形式化证明特性的新型编程语言，其核心目标是通过数学证明来拦截 AI 生成代码中的错误，并能在图形处理器上高效运行。
该项目认为，在后通用人工智能时代，人类终将停止编写和阅读代码，但依然需要一种消除歧义的方式来向构建世界的 AI 表达需求。通过“定律”，人类的意图可以比自然语言更加精确；通过“证明”，可以验证 AI 是否正确实现了提示词要求；再借助快速的编译器，程序能够全速运行。
核心特性
1. 运行速度极快
Bend 直接编译为机器原生代码。在单核处理器上，其运行速度接近 C 语言；同一套二进制程序还可以扩展到 16 核处理器或图形处理器上运行，速度可达单核的数十倍乃至上百倍。在苹果 M4 Max 芯片上运行生命游戏测试中，TypeScript 耗时 18.8 秒，Lean 耗时 13.8 秒，C 语言耗时 6.78 秒，而 Bend 单核耗时 7.80 秒，16 核耗时 0.65 秒（加速 12 倍），图形处理器耗时仅 0.06 秒（加速 124 倍）。
2. 编译与类型检查极快
Bend 的类型检查器同时也是证明检查器，类似于 Lean 和 Rocq。传统工具在中等规模代码库上可能需要数分钟，而 Bend 最多仅需一秒左右，方便 AI 智能体在每次修改代码后即时检查。在处理 3200 个泛型实例化测试中，Isabelle 和 Agda 耗时均超过 5 分钟，Lean 耗时 19.2 秒，Rocq 耗时 6.04 秒，Bend 仅耗时 0.38 秒。
3. 天然的大规模并行
编写 Bend 代码不需要手动管理线程、锁机制或编写计算内核。开发者只需将任务拆分成两半，Bend 就会自动将调用分发到系统能找到的每一个核心上，随后再合并结果。例如 pow2.bend 程序可以直接在 4096 个图形处理器核心上并行运行。
4. 依靠证明阻断 AI 错误
为了让开发者敢于信任从未阅读过的代码，Bend 引入了形式化证明机制。开发者可以在 LAWS.bend 文件中声明不可违背的定律，AI 提交的任何代码都绝不能违反这些规则。在给出的示例中，定律规定“玩家不可能获胜”，当要求 AI 为游戏添加“棋盘循环连通”的新功能时：
• 如果没有 LAWS.bend，AI 引入的逻辑漏洞会导致获胜定律被打破，错误代码会被直接合并上线。
• 如果使用了 LAWS.bend，AI 的错误会被直接拦截，AI 必须不断重试，直到构建出阻挡机制并给出数学证明，确保该定律始终成立。合并错误在数学定理层面被完全杜绝。
快速上手与使用建议
• 安装方式：可以通过终端执行官方提供的 Shell 脚本一键安装。
• 配置 AI 智能体：在项目的 AGENTS.md 文件中添加指令，要求 AI 在使用 Bend 时运行 bend guide 学习语法、使用 LAWS.bend 保存重要规则、在提交前运行 bend PROOF.bend 进行校验，并在可能的情况下尽量并行化代码。配置完成后直接对 AI 说明使用 Bend 即可。
• 开发提示：建议要求 AI 为所有绝不能出错的逻辑编写定律，并对所有需要高速运行的部分进行并行化。Bend 目前还处于早期阶段，主要适用于 Linux 和 macOS 系统的后端开发，遇到问题可以向官方提交反馈。
参考资料
• 语言指南：GUIDE.md 包含了完整的语言规范，可在命令行运行 bend guide 查看。
• 理论论文：BendTT 论文介绍了该语言核心采用的仿射依赖类型论。
• 运行时论文：BendRT 论文介绍了适用于中央处理器和图形处理器的并行虚拟机运行时。