Bend – 一种通过证明阻止 AI 错误并在 GPU 上运行的语言

原文 ↗ Hacker News 讨论 ↗

一种名为 Bend 的新编程语言旨在让开发者指定正式的“定律”，由 AI 生成的代码必须满足这些定律；它使用仿射依赖类型系统和 GPU 加速的运行时来快速检查证明。评论者对用机器检查的不变量来约束 LLM 的想法很感兴趣，但也提出了现实担忧：编写完整且正确的定律可能和编写程序一样难，定义不充分的定律可能被钻空子，而当前生态（标准库、易用性、工具链）仍不成熟。围绕该项目还出现了信任问题，包括其自身代码和文档大量使用 AI、此前删除 git 历史，以及相较于成熟证明助手如 Lean 或 Agda 所作出的大胆性能与正确性主张。

项目目标与定位

  • Bend 被描述为一种带有仿射依赖类型理论的语言，旨在证明程序的“定律”，并编译为高效的 CPU/GPU 代码。
  • 核心思路：人类/代理编写一个小型的 LAWS.bend 规格；AI（或人类）编写其余部分；编译器检查所有代码是否满足这些定律。
  • 明确面向“后 AGI”世界以及基于 LLM 的编码代理进行宣传。

仓库历史、信任与 AI 生成代码

  • 人们对 GitHub 仓库被压缩成单一提交、抹去历史、fork 和可复现性这件事有很大担忧；鉴于其宏大主张，这被视为一个信任问题。
  • 在反对意见出现后，历史随后被恢复；有人认为这被夸大了，也有人认为这对审计性和基准测试至关重要。
  • 编译器/文档的大量部分由 LLM 生成或在其帮助下完成；一些人认为这很正常，另一些人则将其视为“AI slop”，并在与宏大主张结合时视作危险信号。

类型系统、证明与“定律”

  • Bend 使用线性/仿射类型和数量索引宇宙，禁止运行时闭包克隆，以确保终止性和良好的 GPU 行为。
  • 定律本质上是编译期检查的不变量/证明；测试被明确对比为不能提供同样的保证。
  • 多位评论者指出一个经典问题：为大型系统指定正确、非空洞的定律，至少和编写代码一样难。
  • 存在“负空间编程”的风险：AI 通过改变问题本身来满足定律（例如游戏移动规则、世界大小），而不是反映用户意图。

性能、GPU 故事与对比

  • 关于相较 Lean/Agda/Isabelle 快一个数量级的证明检查速度的说法，受到了怀疑：
    • Bend 避免了统一、战术和推断，因此将其与功能更完整的 elaborator 比较被认为具有误导性。
    • GPU 的使用目前用于运行时并行性；编译期在 GPU 上进行证明检查“尚未实现”。
  • 有些人对 interaction-net/HVM 的技术谱系感兴趣；也有人指出 Bend 2 在架构上与更早的工作不同。

语言设计、易用性与文档

  • 文档（GUIDE）因雄心勃勃而受到称赞，但也因令人困惑而遭到批评：
    • 关于被擦除参数、Kind 参数、数组语法，以及诸如 Array<T> & U32 之类令人惊讶的类型，都有人提出疑问。
    • 数组/线性性导致 API 不直观（读取返回 (array, value)），作者也承认这可能需要重新设计。
  • 缺少战术和推断使证明变得冗长；作者的立场是，如果 AI 来写证明，那么冗长是可以接受的。

采用、生态与替代方案

  • 人们担心：
    • 标准库很小、缺少数学库，以及将大型现有证明从 Cubical Agda 等系统迁移过来的困难。
    • 工具链缺失或仍处于早期阶段（变更日志、版本发布、与现有语言的集成等）。
  • 有些人对此很兴奋并在试验（例如移植小型应用、会议安排器）；另一些人则更偏好现有工具，如 Lean、Coq、Dafny、Verus，或主流语言中的类证明契约。
  • 多人指出，这是前景不错的早期研究/工程，但当前营销夸大了成熟度和适用范围。