Bend – A language that blocks AI mistakes via proof, on CPU and GPU

Bend – 一种通过证明在 CPU 和 GPU 上阻止 AI 错误的编程语言

Bend is a fast language that blocks AI mistakes via proof. It features C-like speed, CUDA parallelism, Lean-style proofs, and Python-like syntax. Bend 是一种通过证明来阻止 AI 错误的快速编程语言。它具备 C 语言级的速度、CUDA 并行能力、Lean 风格的证明机制以及类似 Python 的语法。

In the post-AGI economy, humans will eventually stop writing and reading code, but we still need an ambiguity-free way to tell the AIs building the world around us what we want done. With laws, our intents can be much more precise than natural language. With proofs, we can verify that the AI implemented our prompts correctly. And a fast compiler runs it at speed. That’s Bend - and nothing else. 在后 AGI 时代，人类终将不再编写和阅读代码，但我们仍然需要一种无歧义的方式来告诉正在构建世界的 AI 我们想要什么。通过“法则”（Laws），我们的意图可以比自然语言精确得多；通过“证明”（Proofs），我们可以验证 AI 是否正确执行了我们的提示词；而快速的编译器则保证了运行速度。这就是 Bend，别无他选。

1. Bend runs FAST.

1. Bend 运行速度极快。

Bend compiles to native code. On one core, it runs nearly as fast as C. The same binary also runs on sixteen cores, or on the GPU, running up to a hundred times faster than one core. Bend 可编译为原生代码。在单核上，它的运行速度几乎与 C 语言相当。同一个二进制文件可以在 16 个核心甚至 GPU 上运行，速度比单核快达百倍。

2. Bend compiles FAST.

2. Bend 编译速度极快。

Bend’s type checker is a proof checker, as in Lean and Rocq. Those can take minutes on a mid-sized codebase. Bend takes a second at most, so an AI agent can check after every change. Bend 的类型检查器本质上是一个证明检查器，类似于 Lean 和 Rocq。后者在中等规模的代码库上可能需要几分钟，而 Bend 最多只需一秒，因此 AI 代理可以在每次修改后进行检查。

3. Bend is PARALLEL.

3. Bend 是并行的。

No threads, no locks, no kernels to write. Split the work in two, and Bend spreads the calls over every core it can find, then joins them back. Now watch pow2 run on 4,096 GPU cores. 无需编写线程、锁或内核。只需将任务一分为二，Bend 就会将调用分配到它能找到的每一个核心上，然后再将结果合并。现在看看 pow2 在 4,096 个 GPU 核心上运行的效果吧。

4. Bend BLOCKS mistakes - with proof.

4. Bend 通过证明来阻止错误。

How can you trust code you never read? By demanding a proof. LAWS.bend is where you declare laws. From then on, no AI can ship one line that breaks them, ever. 你如何信任从未阅读过的代码？通过要求证明。LAWS.bend 是你声明法则的地方。从那时起，任何 AI 都无法提交一行违反这些法则的代码。

LAWS.bend is AGENTS.md backed by proof. “Make no mistakes” is now type-checked. Skeptical? Try breaking the game. LAWS.bend 就是有证明支持的 AGENTS.md。“不出错”现在已成为类型检查的一部分。怀疑吗？试着去破坏游戏规则看看。

5. Get started.

5. 如何开始。

5.1. Install curl -fsSL https://bend-lang.com/install.sh | sh

5.2. Tell your agent to use Bend 5.2. 让你的 AI 代理使用 Bend Add this to your AGENTS.md: 在你的 AGENTS.md 中添加： When using Bend:

• run bend guide to learn it
• use LAWS.bend to keep important rules
• run bend PROOF.bend before committing
• parallelize the code whenever possible Then, just say: “use Bend”! 使用 Bend 时：
• 运行 bend guide 进行学习
• 使用 LAWS.bend 来保留重要规则
• 在提交前运行 bend PROOF.bend
• 尽可能并行化代码 然后，只需说：“use Bend”！

5.3. Enjoy bug-free, fast vibe-coded apps! 5.3. 享受无 Bug、快速且“直觉编码”的应用程序！ Hints: ask it to write laws for whatever should never break, and to parallelize everything you want running fast. Bend is young: if anything goes wrong, ask it to open an issue. Bend works best on the back-end, on Linux and on macOS. Enjoy! <3 提示：要求 AI 为任何绝不能出错的部分编写法则，并为你想要快速运行的所有内容进行并行化。Bend 还很年轻：如果出现问题，请让它提交一个 Issue。Bend 在后端、Linux 和 macOS 上运行效果最佳。尽情享受吧！<3

6. References.

6. 参考资料。

• Guide: GUIDE.md is the whole language; bend guide prints it.
• Paper: BendTT, an affine dependent type theory, Bend’s core.
• Paper: BendRT, a parallel runtime for CPUs and GPUs, the VM.
• 指南： GUIDE.md 包含了整个语言；bend guide 可打印该指南。
• 论文： BendTT，一种仿射依赖类型理论，是 Bend 的核心。
• 论文： BendRT，一种用于 CPU 和 GPU 的并行运行时，即虚拟机。

Bend is still evolving. Expect bugs, and please report them. Bend 仍在不断演进中。可能会遇到 Bug，请务必反馈。