一种通过证明阻止AI错误的快速语言
C 速度 ·CUDA 并行处理 ·精益证明 ·Python 语法
在后通用人工智能（AGI）经济中，人类最终会停止写写和阅读代码，但我们仍然需要一种无歧义的方式，告诉构建我们周围世界的人工智能我们希望做什么。
有了定律，我们的意图比自然语言更精确。通过证明，我们可以验证AI正确实现了我们的提示。而且快速编译器能快速运行它。
Bend会编译成原生代码。在一个核心上，它几乎和C语言一样快。同样的二进制文件也能运行在十六个核心上，或者在GPU上运行，速度可达一个核心的一百倍。
Bend 的类型检查器是证明工具，类似于 Lean 和 Rocq。这些在中等规模的代码库上可能需要几分钟。Bend 最多只需一秒钟，所以 AI 代理可以在每次更改后检查。
没有线程，没有锁，也没有内核可写。把工作分成两部分，Bend 会把调用分散到它能找到的每个核心上，然后再重新连接回去。现在看看 PoW2 在 4,096 个 GPU 核心上运行：
你怎么能信任你从未读过的代码？通过要求证明。LAWS.bend是你宣告法律的地方。从那以后，任何AI都不能发布任何违背规则的行。看它守护一场游戏：
“克洛德，让棋盘环绕”
没有LAWS.bend，这个漏洞就启动了。有了LAWS.bend，AI不得不重试，直到筑起墙并证明定律成立。合并一个漏洞在数学上是不可能的：这是一个定理。
LAWS.bend AGENTS.md 有证据支持。“不要出错”现在是类型校验的。
持怀疑态度？试试破解这个游戏。#lab
提示：让它为那些永远不会出错的事写定律，并并行化你想快速运行的所有东西。Bend还年轻：如果出现问题，让它开一个问题。Bend在后端、Linux和macOS上表现最好。祝你玩得开心！<3
指南：GUIDE.md：https://github.com/bendlang/bend/blob/main/guide/GUIDE.md 是完整的语言；bend guide 会打印它。论文：BendTT：https://github.com/bendlang/bend/blob/main/paper/BendTT.pdf，一种仿射依赖类型理论，是 Bend 的核心。论文：BendRT：https://github.com/bendlang/bend/blob/main/paper/BendRT.pdf，用于 CPU 和 GPU 的并行运行时，即虚拟机。
Bend 仍在不断发展。预计会有错误，请报告它们：https://github.com/bendlang/bend/issues.
a fast language that blocks AI mistakes via proof
C speed · CUDA parallelism · Lean proofs · Python syntax
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.
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'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.
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:
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. Watch it guard a game:
“Claude, make the board wrap around”
Without LAWS.bend, the bug went live. With LAWS.bend, the AI had to retry until it built a wall and proved the law holds. Merging a bug is mathematically impossible: it is a theorem .
LAWS.bend is AGENTS.md backed by proof . “Make no mistakes” is now type-checked .
Skeptical? Try breaking the game.：#lab
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
Guide: GUIDE.md：https://github.com/bendlang/bend/blob/main/guide/GUIDE.md is the whole language; bend guide prints it. Paper: BendTT：https://github.com/bendlang/bend/blob/main/paper/BendTT.pdf, an affine dependent type theory, Bend's core. Paper: BendRT：https://github.com/bendlang/bend/blob/main/paper/BendRT.pdf, a parallel runtime for CPUs and GPUs, the VM.
Bend is still evolving. Expect bugs, and please report them：https://github.com/bendlang/bend/issues.
扫码直达文章详情