弯语言（Bend）是一款通过证明阻断AI错误的快速语言，具备C速度、CUDA并行与精益（Lean）证明。在后AGI经济中，人类终将停止编写和阅读代码，但仍需无歧义方式向构建世界的AI传达意图。借助法则，意图比自然语言更精确；借助证明，可验证AI正确实现了提示；快速编译器使之高速运行。这便是Bend。
正文
Bend 是一门通过证明来阻断 AI 错误的高速语言。具备 C 的速度、CUDA 的并行性、Lean 的证明。
在后 AGI 经济中，人类终将停止编写和阅读代码，但我们仍需要一种无歧义的方式，告诉那些在身边构建世界的 AI 我们想要什么。借助定律（laws），我们的意图能比自然语言精确得多；借助证明（proofs），我们可以验证 AI 是否按提示正确实现；再加上高速编译器，它便能全速运行。这就是 Bend，别无分号。
1. Bend 运行飞快
Bend 编译为原生代码。在单核上，速度几乎与 C 相当。同一二进制也能在十六核或 GPU 上运行，比单核快最高百倍。
（苹果 M4 Max 测试，越低越好）
2. Bend 编译飞快
Bend 的类型检查器即是证明检查器，如同 Lean 和 Rocq。那些工具在中等代码库上可能耗时数分钟。Bend 最多只需一秒，因此 AI 智能体可在每次改动后检查。
（苹果 M4 Max 测试，越低越好）
3. Bend 是并行的
无需线程、锁或内核编写。把工作一分为二，Bend 便将调用分摊到所有能找到的核心，再合并回来。现在看 pow2 在 4096 个 GPU 核心上运行：
（pow2.bend 运行于 GPU）
4. Bend 用证明阻断错误
如何信任从未读过的代码？靠要求证明。LAWS.bend 是你声明定律之处。从此，任何 AI 都无法提交一行破坏定律的代码。看它守护一个游戏：
定律：胜利是不可能的。
目前有效！
新功能：“Claude，让棋盘回绕”
无 LAWS.bend：定律被破坏。AI 错误：已合并。
有 LAWS.bend：定律完好。AI 错误：被阻断！
没有 LAWS.bend 时，bug 上线了。有 LAWS.bend 时，AI 必须重试，直到建起墙并证明定律成立。合并 bug 在数学上不可能：那是一条定理。
LAWS.bend 乃是由证明背书的 AGENTS.md。“别犯错”如今成了类型检查项。
在 LAWS.bend 中声明：
# LAW: 任何走子序列都不会导致胜利。 law you_cant_win: for moves: List<Move> board = replay(start(), moves) is_won(board) == False{}
在 PROOF.bend 中：
# PROOF: you_cant_win holds. def Laws.you_cant_win(moves): # ... written by the AI
5. 开始使用
5.1 安装
curl -fsSL https://bend-lang.com/install.sh | sh
5.2 告诉你的智能体使用 Bend
在 AGENTS.md 中添加：
- 运行 bend guide 来学习它
- 用 LAWS.bend 保存重要规则
- 提交前运行 bend PROOF.bend
- 尽可能并行化代码
然后只需说：“用 Bend！”
5.3 享受无 bug、高速的 vibe-coded 应用
提示：让它为任何不应被破坏的东西写定律，并为任何你想跑快的东西做并行。Bend 还年轻：若出问题，让它开 issue。Bend 在后端、Linux 和 macOS 上效果最佳。享受吧 <3
6. 参考资料
指南：GUIDE.md 是完整语言；bend guide 可打印它。论文：BendTT 为仿射依赖类型论，Bend 的核心。BendRT 是面向 CPU 与 GPU 的并行运行时，即虚拟机。
Bend 仍在演进。预期有 bug，请 报告。
评论
社区对 Bend 2.0 的“用证明阻止 AI 出错”叙事普遍存疑，焦点集中在单 commit 历史引发的可信度危机、形式化验证的实用性，以及技术文档的严谨性；少数开发者认可约束 AI 的思路并愿意试用，作者则呼吁尊重。
质疑单 commit 历史损害项目可信度
- 多个用户指出仓库被压缩为单一提交发布，在强调 AI 信任的时代，抹去开发历史会引发警惕，且让人怀疑代码是否真由模型一次性生成。（较多人）
- 需要引用时，只用一句中文意译： > 信任才是真正的硬通货，而清空历史无疑是让人皱眉头的操作。（@AlexErrant）
认为形式化验证难以扩展且非 AI 时代必需
- 不少人主张形式验证太难、无法套用至大型真实系统；若未来 AGI 足够强，它自能理解需求并直接生成可证明的机器码，无需人类用无歧义语言中转。（较多人）
- 需要引用时，只用一句中文意译： > 能写对任意程序并证明任意性质的 AI，必然也聪明到不必与我们形式化沟通就能弄清意图。（@pron）
质疑技术宣称与语言设计文档质量
- 用户从多方面挑刺：GPU 并行不适合证明搜索、与 Lean 等比较缺乏基准、“仿射依赖类型论”作为前沿课题不太可能由 AI 即兴生成的项目完善、指南中类型与数组示例自相矛盾。（较多人）
- 需要引用时，只用一句中文意译： > 若非噱头，这套子结构依赖类型系统本该登上顶级会议，而非出自带 Fable 论文的随机项目。（@stschaef）
反感将项目贬为 AI 随手生成并为之辩护
- 少数意见认为评论区滥贴“AI 随手生成”不公，AI 辅助工具本就允许模型参与，不能因文档有 AI 痕迹全盘否定其价值。（少数人）
- 需要引用时，只用一句中文意译： > 腻了“AI 随手生成”的嘲讽，这是面向 AI 的工具，难道要作者全手写？（@resonious）
认可用定律约束 AI 的思路并给出落地经验
- 部分试用者认为将不变量写成定律契合智能体开发，但在持续集成中加证明检查更现实；同时指出基础库定律匮乏导致实际证明负担重，且定律易被开发者篡改而失效。（较多人）
- 需要引用时，只用一句中文意译： > 定律想法好，但人们常为了新功能改定律本身，所以部分定律必须冻结，最终判断仍靠人。（@RomanKornev）
作者恳请社区礼貌反馈
- 作者现身说明投入近一年每日十六小时免费开发，请求文明指出缺陷而非人身攻击。（少数人）
有价值的补充
- 实测发现基础库仅内置一个加法交换律定律，排序等常用性质缺失，使得“原则上可证明”与“一个下午可证明”存在巨大鸿沟，需自备大量辅助证明。
- 子结构依赖类型相关已有学术工作未被项目论文引用，应补引以增可信度。
- 将代码与证明同置或融入持续集成，已被证实能部分捕获智能体非理性改动，可作为过渡方案。