Bend
AI summary · Qwen Summary in Chinese Indexed
Original source Bend 是一种强调原生速度、并行执行和基于证明的 AI 编码约束的编程语言。
项目定位
- Bend 是一种快速编程语言，目标是通过证明阻止 AI 编码错误。
- 页面将其特点概括为 C 级速度、CUDA 级并行、Lean 式证明和 Python 式语法。
- 页面认为在 AI 构建应用的场景中，laws 和 proofs 可让意图比自然语言更精确。
运行性能
- Bend 编译到原生代码，页面称单核运行速度接近 C。
- 同一二进制可运行在 16 核或 GPU 上，页面称最高可达单核约 100 倍速度。
- 在 Apple M4 Max 的 Game of Life 示例中，Bend GPU 用时 0.06 秒，单核 7.80 秒，16 核 0.65 秒。
编译与检查速度
- Bend 的类型检查器被描述为证明检查器，类似 Lean 和 Rocq。
- 页面称 Bend 对中型代码库的检查最多约一秒，便于 AI agent 每次修改后检查。
- 在 3,200 个泛型实例化测试中，Bend 用时 0.38 秒，低于 Lean 的 19.2 秒和 Rocq 的 6.04 秒。
并行模型
- 页面称 Bend 不需要手写线程、锁或 kernel。
- 用户可将工作分成两部分，Bend 将调用扩展到可用核心后再合并结果。
- 示例 pow2.bend 可在 GPU 的 4,096 个核心上运行。
用证明阻止错误
- LAWS.bend 用于声明必须保持的规则，页面称之后 AI 不能发布破坏这些规则的代码。
- 示例中声明“无法获胜”的 law 后，AI 修改导致 bug 时会被阻止并重试，直到证明 law 成立。
- 页面将 LAWS.bend 描述为有证明支持的 AGENTS.md，使“不要犯错”可被类型检查。
安装与使用建议
- 安装命令为 curl -fsSL https://bend-lang.com/install.sh | sh。
- 页面建议在 AGENTS.md 中要求 agent 运行 bend guide、使用 LAWS.bend、提交前运行 bend PROOF.bend，并尽量并行化代码。
- 页面称 Bend 最适合后端，并在 Linux 和 macOS 上表现最好。
参考资料与状态
- GUIDE.md 被描述为完整语言指南，bend guide 可打印它。
- BendTT 论文描述其核心为仿射依赖类型理论，BendRT 论文描述 CPU/GPU 并行运行时。
- 页面称 Bend 仍在演进，可能存在 bug，并邀请用户报告问题。