Bend：用证明挡住 AI 写错代码的快速语言
来源: bend-lang.com — 2026-09
概述
Bend 自称是一门「用证明挡住 AI 犯错」的快速语言：语法像 Python，编译成原生代码，单核性能接近 C，同一份二进制还能吃满多核甚至 GPU。它的类型检查器同时是证明检查器，允许在 LAWS.bend 里声明不变量，AI 改出来的代码只要违反定律就无法合并。官网给出的安装方式只有一行命令，随后要求在 AGENTS.md 里加上四条使用约定。
核心要点
- 安装后只需往 AGENTS.md 加几行，AI 代理就会用 bend guide 学语言、用 PROOF.bend 在提交前自证。
- 官方叙事是「后 AGI 经济里人类终将不再读写代码」，但仍需要一个无歧义的方式告诉 AI 要什么。
- 多数证明检查器（Lean、Rocq）在中等代码库上要花几分钟，Bend 最多一秒，AI 代理可以在每次改动后都检查。
- 并行模型里没有线程、锁和手写 kernel：把工作一分为二，Bend 自动铺满所有核心再合并，pow2 可跑在 4096 个 GPU 核心上。
- 示例中「胜利不可能」这条定律让 AI 绕开 bug 去建墙并证明定律成立，合并一个 bug 在数学上变成不可能。
金句
你怎么能信任自己从未读过的代码？方式是索要一个证明。
👍 0
👎 0
返回 Lobsters 首页