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 輔助開發交匯處一項值得注意的實驗。