Bend 用数学证明拦住 AI 写错的代码

新编程语言 Bend 的出发点是：AI 智能体（Agent）写出的代码不靠人去读，而是要求它给出证明。Bend 的类型检查器同时就是证明检查器，思路与 Lean、Rocq 一致。团队强调的差别在速度：后两者在中等规模代码库上可能要跑几分钟，而 Bend 最多只要一秒，因此智能体可以在每次修改后都跑一遍检查。

规则写进 LAWS.bend

规则声明在一个名为 LAWS.bend 的文件里。一旦在其中确立了某条法则，任何 AI 都无法提交违反它的一行代码。项目页面展示的游戏示例中，没有 LAWS.bend 时缺陷直接上线；有这个文件时，AI 必须反复重试，直到证明该法则成立为止。团队的说法是：合入一个缺陷在数学上不可能，因为它已经是一条定理。他们把这种做法概括为“有证明背书的 AGENTS.md”。

单核接近 C，GPU 上并行

Bend 编译为原生代码。在单核上运行速度接近 C，同一个二进制文件也能跑在十六个核心上，或者跑在 GPU 上，速度最高可达单核的一百倍。开发者不需要写线程、锁或 kernel：把工作一分为二，Bend 会把调用铺到它能找到的每个核心上，再把结果合并回来。页面上的一个示例演示了 pow2 函数在 4096 个 GPU 核心上运行。

语言的完整文档在 GUIDE.md 中，执行 bend guide 命令即可打印。两篇论文介绍了内部实现：BendTT 是其核心的仿射依赖类型理论，BendRT 是面向 CPU 与 GPU 的并行运行时。项目仍在演进，目前在后端场景、Linux 与 macOS 上表现最好，团队提醒会有缺陷并希望用户提交反馈。详情见项目网站。