AI 编程助手把写代码的成本压到接近零之后，瓶颈换了个位置：你不敢直接合并它写的东西。9 月 17 日，Higher Order Company 发布了编程语言 Bend 2，Hacker News 上相关帖子拿到 470 多分和 220 多条评论。它的定位写在 README 开头：人类最终会停止写代码、读代码，但仍需要一种无歧义的方式告诉 AI 我们要什么。Bend 给出的方案分三层，用法则声明意图，用机器可查的证明验证 AI 的实现，用一个足够快的编译器把验证过的代码跑在 CPU 和 GPU 上。
LAWS.bend：给"别写错"加上编译期强制
常见工作流里，AI 生成的代码靠人来审。Bend 把方向反过来：你在 LAWS.bend 文件里声明应用必须永远成立的规则，编译器要求任何改动代码的 AI 同时交出这些规则仍然成立的证明。证明是数学对象，编译器可以机械检查对错，自然语言承诺做不到这一点。
官方演示是一个小游戏，规则只有一条：玩家不可能获胜。先让 AI 加一个"棋盘边缘环绕"的新功能：
- 没有 LAWS.bend 时，AI 让玩家直接绕过边界拿到旗帜，违反规则的代码被合并。
- 有 LAWS.bend 时，编译器拒绝放行，AI 反复重试，最后给棋盘远端加了一堵墙，然后交出证明，改动才被接受。
墙的位置、旗帜的位置、移动方式，AI 都可以自由发挥；被禁止的只有一个动作，提交一个违反法则的改动，因为这在数学上不可表达，由编译器强制执行。README 给出的声明写法：
# LAWS.bend
law you_cant_win: # "胜利不可能"
for moves: List<Game.Move> # 任意移动序列
board = Game.replay(Game.start(), moves) # 从初始局面重放
{Game.is_won(board) == False{} : Bool} # 永远不会赢
# PROOF.bend
def Laws.you_cant_win(moves):
# ... 由 AI 编写的证明
作者把 LAWS.bend 称作"有证明背书的 AGENTS.md"。README 列出的典型法则包括：账户系统所有余额之和恒为零；玩家不能穿过实心墙；list_sort() 返回升序结果；array_set() 不会越界调用。作者在 Hacker News 评论里举了一个例子：一条"余额之和必须为零"的法则，按他的判断足以在编译期拦下 Ethereum 历史上的 The DAO 攻击，那一次约 360 万枚 ETH 被转出，项目差点因此报废。
同一个类型，两条战线：跑得快，验得也快
能力声明写在官网首页："C speed · CUDA parallelism · Lean proofs · Python syntax"。拆开看。
运行速度。 Bend 编译到原生代码。官方基准（Apple M4 Max）的词法分析器单项：C 用时 1.04 秒，Bend 单核 2.14 秒，16 核 0.20 秒（11 倍加速），GPU 1.07 秒；作为参照，TypeScript 3.54 秒、Lean 4.49 秒。
并行模型。 不写线程、不写锁、不写 GPU kernel。分治风格的递归调用自动铺满所有核心：演示里 pow2(20) 一路分裂，直到每个任务落在 4096 个 GPU 核心之一上，再折叠回收。同一个文件既是 CPU 程序也是 GPU kernel，编译产物是一个 C 文件，按目标平台经宏展开成 Metal 或 CUDA 版本；调用时在表达式后加一个 !，同样的代码就从 CPU 切到 GPU。
检查速度。 Bend 的类型检查器本身就是证明检查器，与 Lean、Rocq 同一血统，但快了数量级。官方 checker 基准（400 smalltt trees）：Isabelle 8.47 秒、Agda 3.27 秒、Lean 1.33 秒、Rocq 1.34 秒、Bend 0.61 秒。这个数字的意义在工作流：传统证明助手检查中等规模代码库要几分钟，AI 每次改动后等不起；Bend 一秒内出结果，agent 可以在每次编辑后立即验证，改完就查。
理论底座：一篇仿射依赖类型理论，外加一份 Lean 形式化
Bend 2 与 Bend 1 不共享血统：README 明确写了旧程序和 HVM 运行时全部不兼容，这是一门从零开始的新语言。理论基础是两篇论文，《BendTT: An Affine Dependent Type Theory》定义语言核心，《BendRT: A Parallel Runtime for CPUs and GPUs》定义运行时。仓库里还有一份 bend.lean，用 Lean 把语言核心形式化了一遍，理论声明的机器可查形态，两条实现可以互相核对。
对大多数读者，需要知道的三点：
- 语法长得像 Python，但所有东西都要标注类型，没有类型推断。全标注是刻意设计，AI 生成和证明检查都因此更直接。
- 值是仿射的（affine）：闭包和数组不能共享，每个值至多使用一次。这个约束换来的正是 GPU 并行时的性能性质。
- 递归必须能证明终止，无限循环在类型层面就写不出来；确有需要时用
@unsafe显式关闭检查。
Hacker News 上有语言理论背景的评论者把 Bend 2 定位为"带仿射改动的定量类型理论"（QTT），擅长平衡递归的代数数据类型计算并自动并行化，但在稠密矩形数组计算上不会比 CUDA 或 Futhark 更强。作者的回应是：目前只内置了很简单的调度器，仍需手动调优，调度器改进在计划内。
Hacker News 上的真问题：法则写不全怎么办
220 多条评论里最有价值的部分，是演示自己暴露的边界。有评论者复现官方 demo 的"移除墙壁"实验：只保留"你不可能获胜"这一条法则，让 AI 把棋盘改成环绕边界，结果 AI 把移动方式改成了对角线，向上向下走正对角线，向左向右走负对角线。法则确实没被打破，游戏确实赢不了了，但游戏已经不是原来那个游戏。跟帖里有人重复实验，得到另一种"创造性合规"：AI 把旗帜所在格子变成不可进入的力场。
作者本人在评论里承认：法则只保护你记得写下的东西，单条"你不可能获胜"严重欠规格，demo 只为展示法则不可被打破，不为展示 AI 会按你的意图行事。他的辩护是：一条小法则就能覆盖一整类 bug，"余额之和为零"一行字防住 The DAO 级别的漏洞，性价比极高。批评者的反驳同样直接：当写法则本身变成比写代码更大的负担，每个程序都会欠规格，"符合法则字面、违背作者本意"的解法会层出不穷。
这场讨论框定了此类工具的适用位置：法则适合表达不变量，不适合表达完整意图。余额守恒、排序后序、数组边界，这类一句话说得死的约束是法则的主场；"用起来顺手"这类模糊意图，法则管不了，也不该由它管。
现在能用吗：先看这串限制清单
README 的 Limitations 一节有 30 多条，密度超过多数项目的功能列表。影响最大的几条：
- 数字只有 Nat、U32、F32：没有 U64、I64、F64（Metal 不支持 f64）；F32 是公理化的，浮点行为无法证明任何性质。
- 字符串是字符链表，文本处理慢；没有 JSON、正则、HTTP、TLS 库，目前可以自己用 foreign 机制接。
- 没有类型类、没有 trait、没有宏（编译期模板除外）；没有 if-else 语法，分支写成对 True/False 的 match。
- 编译到原生很慢（要过 clang/CUDA/Metal），快速迭代用 JavaScript 目标，但 JS 目标单核运行、无图形无音频。
- 每个程序一个 C 文件：没有分离编译，没有增量构建。
- 仓库被压成了一个 commit。作者在评论里的解释是提交历史混有私人数据和 SupGen 的专有代码，顺手压掉了。这引发了信任争论：一个两万 star 的语言仓库没有历史，论文基准里钉的 commit SHA 无从复现。也有人指出 star/fork 比例（约 20938:549）与 F*、Carp 等同类语言一致，增长曲线并不异常。
最后还有一条容易被略过的：编译器 99% 由 AI 编写，官方原话是"尚未经过完整审计"。用它验证 AI 代码之前，先接受一个前提，验证器本身也是 AI 写的，而且没人完整读过它。
它移动的是哪条边界
证明助手和形式化验证存在了几十年，Bend 做的事是把这条技术栈的三个门槛（写得慢、验得慢、跑得慢）同时压到 AI agent 能全程使用的水平：声明意图的成本降到一份 LAWS.bend，验证的成本降到一秒以内的编译检查，执行的门槛降到同一份代码跑 CPU 和 GPU。代码审查里"机器可查"的部分（不变量是否成立），从人眼移交给了编译器；"机器不可查"的部分（意图是否被理解），原样留给人类。
对每天在用 coding agent 的人，现在就能做的实验很具体：curl -fsSL https://bend-lang.com/install.sh | sh 装上，按官方模板在 AGENTS.md 里加四行（跑 bend guide 学语言、用 LAWS.bend 守规则、提交前跑 bend PROOF.bend、能并行就并行），然后把一个后端小工具交给它写一次，观察法则拦下的错误和法则放过的错误各是什么。仓库在 github.com/bendlang/bend，两篇论文在仓库 paper/ 目录，语言核心的 Lean 形式化在 bend2/bend.lean。