Bend 语言发布 – 具备 AI 验证法则的快速 CPU/GPU 编译

Bend 声称提供的功能

Bend 承诺带来三大核心优势：

原生级执行速度 – 编译后的二进制文件在单核 CPU 上运行速度几乎与 C 语言相当，而在 16 核 CPU 或 GPU 上速度可提升至 124 倍。
即时证明检查 – 类型检查器即证明检查器，能在不到一秒的时间内验证用户定义的法则，比 Isabelle、Agda、Lean 或 Coq 在同类代码库上的速度快得多。
自动并行化 – 无需显式的线程或内核代码；运行时会自动将任务分配到所有可用的 CPU 或 GPU 核心，并自动合并结果。

这些声明在 Bend 网站上通过基准测试（如生命游戏、pow2 等）以及一个简短的演示进行了展示，该演示通过“获胜是不可能的”这一法则阻止了一个 AI 生成的 Bug。

Bend 编译为原生机器码。在 Apple M4 Max 处理器上，报告的运行时间为：

该网站将这些数据与 TypeScript (18.8 s)、Lean (13.8 s) 和 C (6.78 s) 进行了对比。GPU 基准测试在 4,096 个 GPU 核心上运行相同的二进制文件，展示了运行时无需用户编写内核即可利用大规模并行性的能力。

Bend 引入了 LAWS.bend，这是一个开发者声明必须始终遵守的不变量的文件。当 AI 代理（例如 Claude）生成代码时，编译器会根据声明的法则检查生成的 PROOF.bend。如果违反了法则，编译将失败，AI 必须重试，直到生成证明该法则成立的证明为止。

法则示例（无获胜序列）：

# LAW: no move sequence leads to victory.
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):
  # ... AI‑generated proof

系统将法则视为一种类型；任何违反该法则的代码都会在编译时被拒绝。

BendRT 是一个运行时，它能自动将纯函数调用分发到可用核心上。该语言不需要显式的线程创建、锁管理或编写 CUDA 内核。工作被拆分、并行执行，结果被透明地合并。演示展示了一个 pow2.bend 程序通过单条命令在 4,096 个 GPU 核心上运行。

证明工作量： 几位评论者指出，编写必要的法则和证明可能非常耗时。一位用户报告称，为了一个简单的日历 cron 任务，需要编写约 60 行基础算术引理。
工具缺口： 人们提出了关于系统如何与现有库集成、证明是否可以在项目间重用，以及如何处理缺失或错误法则的问题。
仓库透明度： GitHub 仓库显示只有一个最近的提交，没有可见的提交历史，这引发了对项目成熟度和可信度的质疑。
性能限制： 一些观察者将 Bend 的 GPU 性能与 Futhark 等专用语言进行了比较，并指出平衡的递归工作负载适合 Bend，而密集的数组内核可能会滞后。
强制保证： 用户询问是什么阻止了 LLM 简单地忽略法则；答案是编译器会拒绝任何未提供有效证明的生成代码，但仍需引导 AI 生成此类证明。

"LAWS.bend 是由证明支持的 AGENTS.md。‘不出错’现在已成为类型检查的一部分。” – Bend 网站

“我最想要的法则：‘没有两个输出计划重叠。’ 我没有声明它。它需要 collapse 输入的有序性作为假设……这才是衡量‘原则上可证明’与‘今天下午就能证明’之间差距的诚实尺度。” – svachalek

“2 万个星标，一小时前只有一个提交？这是献祭了多少只山羊？” – plastic041（对仓库历史表示担忧）

安装（使用单个脚本）：

curl -fsSL https://bend-lang.com/install.sh | sh

Bend 是一个非常早期的项目；请预料到会有 Bug 和快速迭代。欢迎通过 GitHub 问题跟踪器提交贡献和问题报告。