curl -fsSL https://bend-lang.com/install.sh | sh
使用 Bend 时：
- 运行 `bend guide` 来学习它
- 使用 `LAWS.bend` 来保存重要规则
- 在提交前运行 `bend PROOF.bend`
- 尽可能并行化代码
一门快速的语言，通过证明来阻止 AI 犯错
C 的速度 · CUDA 的并行 · Lean 的证明 · Python 的语法
在后 AGI 经济中，人类最终将不再编写和阅读代码，但我们仍然需要一种无歧义的方式，来告诉那些正在构建我们周围世界的 AI 我们想要完成什么。
借助定律，我们的意图可以比自然语言精确得多。借助证明，我们可以验证 AI 是否正确实现了我们的提示。而一个快速的编译器能以极快的速度运行它。
这就是 Bend——别无其他。
Bend 编译为原生代码。在单核上，它的运行速度几乎与 C 一样快。同一个二进制文件也能在十六个核心上运行，或在 GPU 上运行，速度最高可达单核的一百倍。
Bend 的类型检查器就是一个证明检查器，如同 Lean 和 Rocq 那样。那些工具在中等规模的代码库上可能需要几分钟。Bend 最多只需一秒，因此 AI 代理可以在每次更改后进行检查。
无需线程，无需锁，无需编写内核。将工作一分为二，Bend 就会把调用分散到它能找到的每一个核心上，然后再将它们合并回来。现在看看 pow2 在 4,096 个 GPU 核心上运行：
你如何信任自己从未读过的代码？通过要求一份证明。
LAWS.bend 是你声明定律的地方。从那时起，任何 AI 都无法
交付一行违反它们的代码，永远不能。看看它如何守护一个游戏：
定律：获胜是不可能的
新功能：
“Claude，让棋盘环绕起来”
没有 LAWS.bend：
有 LAWS.bend：
没有 LAWS.bend，这个 bug 上线了。有了 LAWS.bend，AI
不得不重试，直到它建起一堵墙并证明该定律成立。
合并一个 bug 在数学上是不可能的：这是一个定理。
LAWS.bend
# 定律：没有任何移动序列能导致胜利。
law you_cant_win:
for moves: List<Move> # 任意移动序列
board = replay(start(), moves) # 从初始状态重新执行
is_won(board) == False{} # 永远不会导致胜利
PROOF.bend
# 证明：you_cant_win 成立。
def Laws.you_cant_win(moves):
# ... 由 AI 编写
LAWS.bend
是 AGENTS.md
由证明支撑。
“不要犯错”现在经过类型检查。
curl -fsSL https://bend-lang.com/install.sh | sh
将此添加到你的 AGENTS.md
:
使用 Bend 时：
- 运行 `bend guide` 来学习它
- 使用 `LAWS.bend` 来保存重要规则
- 在提交前运行 `bend PROOF.bend`
- 尽可能并行化代码
然后，只需说：“使用 Bend”！
提示：让它为任何永远不应破坏的事物编写法则，并将你想要快速运行的一切并行化。Bend 还很年轻：如果出现任何问题，请让它打开一个问题。Bend 在后端、Linux 和 macOS 上表现最佳。享受吧！<3
指南：GUIDE.md 是完整的语言说明；bend guide
会打印它。
论文：BendTT，一种仿射依赖类型理论，Bend 的核心。
论文：BendRT，用于 CPU 和 GPU 的并行运行时，即虚拟机。
Bend 仍在不断发展。预计会有错误，请报告它们。