Bend 語言發布 – 具備 AI 防護法則的高速 CPU/GPU 編譯器

Bend 聲稱提供的功能

Bend 承諾帶來三大核心優勢：

原生速度執行 – 編譯後的二進位檔案在單個 CPU 核心上運行速度幾乎與 C 語言相當，而在 16 核心或 GPU 上則可快達 124 倍。
即時證明檢查 – 其型別檢查器同時也是證明檢查器，能在不到一秒的時間內驗證使用者定義的法則 (laws)，速度遠快於在類似程式碼庫上使用 Isabelle、Agda、Lean 或 Coq。
自動平行化 – 無需編寫顯式的執行緒或核心程式碼；執行時期會自動將工作分配到所有可用的 CPU 或 GPU 核心，並自動合併結果。

這些聲明在 Bend 網站上透過基準測試（如生命遊戲、pow2 等）以及一個簡短的演示進行了展示，該演示利用「獲勝是不可能的」這一法則成功阻擋了一個由 AI 生成的錯誤。

高速編譯與執行

Bend 可編譯為原生機器碼。在 Apple M4 Max 處理器上，報告的執行時間如下：

1 核心： 7.80 s (≈1× C 語言的 6.78 s)
16 核心： 0.65 s (≈12× 加速)
GPU： 0.06 s (≈124× 加速)

該網站將這些數據與 TypeScript (18.8 s)、Lean (13.8 s) 和 C (6.78 s) 進行了比較。GPU 基準測試在 4,096 個 GPU 核心上運行相同的二進位檔案，展示了該執行時期在無需使用者編寫核心程式碼的情況下，利用大規模平行運算的能力。

用於阻擋 AI 錯誤的基於證明的「法則」

Bend 引入了 LAWS.bend，這是一個開發者用來宣告絕不能違反的不變量 (invariants) 的檔案。當 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)

BendRT 是一個自動將純函數呼叫分配到可用核心上的執行時期。該語言不需要顯式的執行緒建立、鎖定管理或編寫 CUDA 核心。工作會被拆分、平行執行，並透明地合併結果。演示顯示 pow2.bend 程式只需一個指令即可在 4,096 個 GPU 核心上運行。

Hacker News 上的社群反應

讚賞與好奇

使用者讚賞將快速原生編譯與針對 AI 生成程式碼的形式化驗證相結合的創新做法。
有些人看到了在排程或合約執行等領域進行基於不變量開發的潛力。

懷疑與實際考量

證明工作量： 幾位評論者指出，編寫必要的法則和證明可能非常耗時。一位使用者報告稱，為了完成一個簡單的日曆 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

將指引加入 AGENTS.md，以便 AI 代理知道在提交前執行指引、使用法則並呼叫證明檢查器。
為關鍵不變量編寫法則，然後讓 AI 生成程式碼及相應的證明。
執行編譯後的二進位檔案（在 CPU 或 GPU 上）；執行時期會自動進行平行化。

開放性問題與未來工作

證明的可擴展性： Bend 如何處理枚舉所有移動序列不可行的極大狀態空間？
互操作性： Bend 是否會提供 FFI 綁定以呼叫現有的 C/Rust 函式庫，或提供將 Bend 程式碼嵌入大型專案的方法？
工具成熟度： 社群要求提供變更日誌、版本化發布以及更清晰的提交歷史以建立信任。
基準測試： 獨立的效能測量（例如在 Bells 基準測試套件上）將有助於驗證所聲稱的加速效果。

參考資料

指南： 儲存庫中的 GUIDE.md（完整的語言規範）。
BendTT 論文： 該語言底層的仿射依賴型別理論。
BendRT 論文： CPU 和 GPU 平行執行時期的說明。

Bend 是一個非常早期的專案；請預期會有錯誤並進行快速迭代。歡迎透過 GitHub 問題追蹤器提交貢獻和問題報告。