Bend编程语言：用证明拦截AI代码错误

Bend 是什么

Bend 是一门新公开的编程语言，官网 bend-lang.com 的定位是"一门通过证明拦截 AI 错误的高速语言"，标语是"C 的速度、CUDA 的并行、Lean 的证明、Python 的语法"。官网设定的背景是：在"后 AGI 经济"里，人类会逐渐不再自己写代码、读代码，但仍需要没有歧义的方式告诉负责实现代码的 AI 自己想要什么——用"法律（laws）"代替自然语言描述意图，用"证明（proofs）"验证 AI 是否真按法律实现了代码，再靠足够快的编译器把结果跑起来。

安装是一行命令：curl -fsSL https://bend-lang.com/install.sh | sh。官网建议的用法：先跑 bend guide 学习语言，把"不能违反的规则"写进 LAWS.bend，每次提交前跑一遍 PROOF.bend，并尽量让代码并行执行。

证明机制怎么拦截错误

Bend 把"类型检查"做成"证明检查"，与 Lean、Rocq 这类证明助手同类。官网称，这类工具检查中等规模代码库通常要花几分钟，而 Bend 最多一秒完成，因此 AI agent 可以在每次改动后都跑一次检查。

官网的示例是一个棋盘类游戏：开发者要求"Claude, make the board wrap around"（让棋盘环绕）。没有 LAWS.bend 时，AI 实现的改动带着 bug 直接合并上线；写下"任何走法序列都不能导致胜利"这条规则后，AI 必须反复重试，直到实现出一堵墙、并证明该规则依然成立，改动才能通过。官网称这让"合并一个 bug 在数学上变得不可能——它是一条定理"。

开发者在 LAWS.bend 里声明规则（如 law you_cant_win），AI 在 PROOF.bend 里写出对应证明函数。官网把这套机制类比为"带证明的 AGENTS.md"：把规则写进 AGENTS.md，对 AI 说一句"use Bend"，之后 AI 生成的代码都要先通过证明检查。

CPU 与 GPU 双跑，目前仍在早期

性能上，官网称 Bend 编译成原生代码：单核接近 C 语言速度；同一份二进制也能跑在 16 个核心，或直接跑在 GPU 上，比单核最多快上百倍——例子是 pow2 函数被拆分后跑在 4096 个 GPU 核心上。这个过程不需要开发者自己写线程、锁或 GPU kernel：把任务拆成两份，Bend 会把调用分散到能找到的每个核心，再把结果合并回来。

官网明确项目仍处于早期：目前在后端场景、Linux 和 macOS 上运行效果最好；原话是"Bend is still evolving. Expect bugs, and please report them"，遇到问题建议直接让 AI 帮忙提交 issue。官网没有给出下一版本或路线图的具体时间点。