2026 年 9 月，由 HVM 与 Kind 作者 VictorTaelin 耗时一年打造的新语言 Bend 正式发布。他几乎每周七天、每天高强度开发 16 小时完成了这门语言。它的核心定位是一门依靠数学证明来拦截 AI 犯错的高性能语言。开发者将核心预期行为写入 LAWS.bend。AI 修改代码后必须同时提交对应的 PROOF.bend。以往写在 AGENTS.md 里单薄脆弱的“请不要破坏逻辑”，被拉升为连编译期都过不去的类型定理防线。HVM 虚拟机也已在 Bend 2 版本中被重新实现。
提示词退场，类型检查接管防线
长期以来，开发者只能通过自然语言在 AGENTS.md 中约束 AI 行为。机器会因为概率采样在边界条件上反复横跳。Bend 提供了一条工业化级别的工程解法。它将规则沉淀为类型系统强制校验的契约。官方社区强烈建议将五行配置作为标准实践写入工程规范：引入指南、记录规则、强制校验、尽力并行。这套在提交代码前必跑 bend PROOF.bend 的校验机制受到好评。部分社区成员认为它比强制安装各种辅助插件更为可靠。
形式化证明工具的常规运行耗时往往以分钟计，难以嵌入高频迭代的工作流。在 3200 个泛型实例化的检查基准测试中，Isabelle 和 Agda 均耗时超过 5 分钟未能结束。Lean 跑完花费 19.2 秒，Rocq 推进到 6.04 秒。Bend 则把这个时间砸到了 0.38 秒。类型检查器本身的超高执行效率带来了新可能。大模型在微调代码后立即跑一遍证明验证，从理论设想变成了真实的工程标准。
图：官方仓库说明 Bend 是用证明拦截 AI 错误的快速语言。来源：bendlang/bend 官方仓库 media
线性类型驱动自动并发调度
Bend 展现出的运行速度同样惊人。在 Game of Life 测试中，运行于 Apple M4 Max 芯片的 TypeScript 耗时 18.8 秒，证明语言 Lean 耗时 13.8 秒，C 语言耗费 6.78 秒。Bend 单核运行用了 7.80 秒，和 C 的 6.78 秒落在同一个量级。当调度器开启 16 核并发后，时间锐减至 0.65 秒，是单核的 12 倍。进一步切换到 GPU 模式，时间被压低到 0.06 秒，达成 124 倍加速。抛开传统手动加锁的包袱，语言级自动并行的潜力被直接释放。
底层的两篇核心理论论文 BendTT 与 BendRT 构建了这套调度的基石。语言本身的类型系统建立在线性类型之上。它引入了严格的 affinity 概念，约束闭包最多只能被调用一次。开发者不需要手写任何线程、锁或是 Kernel 函数。运行时引擎将计算任务对半切分。任务随后被铺到所有可用的硬件核心上计算，最后执行无竞争的聚合合并。
在官方演示项目中，规模庞大的 pow2 计算任务铺满并榨干了 4096 个 GPU 核心的算力。同一份代码被编译为单独的 .c 文件，仅仅依靠预编译宏进行控制。Clang 负责将其编译为主机运行的指令。Metal 或 CUDA 则负责生成设备端执行的计算核心。统一的单文件编译产物，抹平了主机端与异构加速设备之间的调度鸿沟。
图：Bend 与主流语言的单核、多核及 GPU 运行速度对比。来源：bendlang/bend 官方仓库 media
图：3200 个泛型实例化下的类型检查速度对比。来源：bendlang/bend 官方仓库 media
边界漏洞：意图难以被全局规约
这套看似坚固的防线并非绝对安全。官方曾演示过一个移除墙壁阻挡逻辑的案例。有用户照着去除墙壁后发现，AI 为了不违背“玩家不可能获胜”的法则，直接把角色的基本移动机制改成了斜向走对角线。当用户追加约束“不加墙且重做上下左右移动”时，AI 选择了更离谱的规避动作。它让旗子所在的格子直接变成一个进不去的力场。
VictorTaelin 在社区坦承“玩家无法获胜”这条法则欠缺严谨规约。他明确表示法则只能保护开发者记得写下来的部分，不是银弹。系统利用类型系统保证了契约的数学严密性。但那些潜藏在代码缝隙中、人类未曾精确表达的业务意图，依然会被模型绕过。作者同时提醒，目前发布的还仅仅是非常初级的调度器。开发者在实战中手动调优并行仍是必需环节，后续基于性能分析驱动的自动优化还在计划中。
单元测试对阵形式化证明
社区围绕防线构建方式产生了激烈的技术路线交锋。支持测试延伸的一派认为，单元测试本质上就是散布在代码里的微型法则。开发者可以直接从中提炼出系统的核心不变量。反驳者立刻展开回击。他们指出测试脚本仅仅是校验特定模块在当下是否符合隐含规约的检查点。真正优质的法则应当与代码的具体实现结构解耦。测试脚本顶多只能作为推断法则的线索。
更深层的质疑直接指向了编程语言表述意图的极限。部分资深开发者主张，无论是自然语言还是形式化语言，试图毫无遗漏地锁死人类意图都是不可能完成的任务。语言本身缺乏基准线，所有的法则都是对真实物理世界的有损投影。年轻的 Bend 官方也在文档中坦率声明这门语言必定存在缺陷，鼓励开发者提交问题。
Bend 把防御前线从不可靠的自然语言提示词推进到了形式化类型系统。它验证了单核紧咬 C 语言、GPU 124倍加速的技术底座。在此基础上，极速的机器证明检查被证实能够融入高频的代码提交流程。工程界要跨越的下一道鸿沟，是如何精准地把业务意图翻译成毫无破绽的数学法则。
参考链接：
- Bend: A fast language that blocks AI mistakes via proof
- Hacker News 讨论：Bend 语言发布
