bendlang/bend

Bend – 一门具备内置证明的高性能并行语言

简介 – Bend 是一门开源编程语言，结合了高性能编译器（目标是在 CPU 上达到 C 级别速度，在 GPU 上达到 CUDA 级别速度）与证明辅助类型系统。该语言允许你在名为 LAWS.bend 的文件中编写 laws（形式化规范）；编译器要求任何代码变更都必须提供数学证明，以确保这些规范永远不会被破坏。它的定位是让 AI 生成的代码在无需人类逐行阅读的情况下变得值得信赖。

核心理念

• 快速执行 – 强大的静态类型、纯粹性与线性特性，让编译器能产生与手写代码一样快，甚至能扩展至数千个 GPU 核心的原生 C、Metal、CUDA 或 JavaScript 代码。
• 快速验证 – 同一个编译器能在不到一秒的时间内检查证明，远快于 Isabelle、Agda、Lean 或 Coq 等传统证明辅助工具。
• 隐式并行 – 无需明确的线程或锁；运行时会自动将纯计算分配到所有可用的 CPU/GPU 核心并合并结果。
• 规范驱动开发 – LAWS.bend 文件编码了不变量（例如：“所有余额的总和必须为零”）。当代码被编辑时，编译器会要求提供证明以确保不变量仍然成立，从而阻挡任何会违反该规范的 AI 生成变更。

典型工作流程

1. 在 LAWS.bend 中编写一个或多个规范。
2. 要求 LLM（或人类）实现或修改代码。
3. 运行 bend PROOF.bend – 编译器会根据规范检查证明。
4. 若证明成功，代码将编译为快速的可执行文件；否则变更将被拒绝。

语法示例（类似 Python 并具备依赖类型）

import Base

def main() -> IO(Unit):
  do IO<Unit>:
    name : String <- IO.try(String, IO.get_env("USER"))
    IO.print("Hello, " ++ name)

一个规范及其证明：

law add_zero:
  for x: Nat
  {Nat.add(x, 0n) == x : Nat}

def add_zero(x):
  match x:
    case 0n: {==}
    case 1n+xp:
      %add_zero(xp) : {1n+Nat.add(xp, 0n) == 1n+_ : Nat}
      {==}

仓库中的关键组件

• bend2/ – 编译器与标准库 (base.bend)。
• paper/ – 描述类型理论 (BendTT) 与并行运行时 (BendRT) 的学术 PDF。
• bench/ – 用于性能图表的基准测试程序。
• tools/bend-fmt-lsp – 提供仅限语法之语言服务器功能的格式化工具/LSP。
• demos/ – 小型示例应用程序，每个应用程序都有自己的 LAWS.bend。

安装

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

该脚本会安装 bend 命令行工具，可用于编译、运行 bend guide、格式化代码等。

当前限制（如 README 所列）

• 代码冗长：所有内容都必须标注；没有类型推断。
• 没有类型类、特征或编译时模板以外的宏。
• 缺乏证明搜索/策略；证明必须手动编写。
• 仿射值意味着闭包/数组无法自由共享。
• 标准库有限（无 TLS、HTTP、JSON、regex 等）。
• 仅限单文件程序；无增量构建。
• GPU 支持限制为每个程序一个设备；无多机执行。
• Windows 非首要目标（WSL 可运行）。JavaScript 目标为单线程执行。
• 工具极简：仅有格式化 LSP，无调试器、性能分析器、REPL 或丰富的诊断功能。
• 编译器本身很大程度上是由 AI 生成的，尚未经过全面审计。

社区与资源

• 网站：https://bend-lang.com
• Discord、Twitter/X、Reddit 与 GitHub issues 用于支持与讨论。
• 完整语言指南 (GUIDE.md)、正式 Lean 模型 (bend.lean) 与学术论文以供深入了解。

总结 – Bend 是一门真实且积极维护的语言项目，旨在满足 AI 系统生成可验证、高性能代码的新兴需求。它仍处于早期阶段，缺少许多便利功能，但其核心承诺——快速执行 与 快速证明检查——使其成为系统编程、形式化验证与 AI 辅助开发交汇处一项值得注意的实验。