編按：本文綜合整理自 Bend 官網、GitHub HigherOrderCo/Bend、Hacker News 討論串（49746163），並加入 Siami 編輯部觀點與分析。
一門叫 Bend 的程式語言正在 Hacker News 上以 139 分、60 則留言的熱度衝榜。它的賣點不是「更快」，而是「讓 AI 寫的程式碼數學上不可能犯錯」。
Bend 在做什麼
開發者 Victor Taelin（巴西，Higher Order Company）把 Bend 定位為「後 AGI 經濟」的程式語言。當人類不再親自寫 code，我們還是需要一種「沒有歧義的方式」告訴 AI 我們想要什麼。Bend 給的答案是兩件武器：
- Laws（法則）：用
LAWS.bend檔案宣告「永遠不能發生」的事，例如「沒有任何一連串移動能導致玩家獲勝」。 - Proofs（證明）：用
PROOF.bend讓型別檢查器（type checker）證明那段程式碼遵守所有法則。
如果 AI 寫出違反法則的程式碼，編譯就會失敗。不是測試抓到、不是 code review 抓到，而是根本合不進 build 系統。官網示範一個小遊戲：
不加
LAWS.bend：AI 把「讓棋盤繞一圈」寫成 merge bug，直接上線。 加LAWS.bend：AI 必須重新嘗試，直到它在「贏不可能」的證明下建出一面牆。合併 bug 在數學上變成不可能，因為它本身就是個定理。
速度宣稱：接近 C、原生平行、4096 顆 GPU 核心
官網給出三組基準（Bench on Apple M4 Max）：
- 單核：Bend 編譯成原生碼，跑起來幾乎跟 C 一樣快。
- 多核：同一個 binary 跑在 16 核上，或直接跑在 GPU 上，最高比單核快 100 倍。
- 平行無痛：沒有 thread、沒有 lock、沒有手寫 CUDA kernel。「把工作切成兩段」Bend 自動把呼叫散到所有可用的核心再 join 回來。
最有戲劇張力的展示是 pow2.bend——一段普通函式直接跑在 4,096 個 GPU 核心上，沒有任何 GPU 程式碼。底層是 Bend 1 開始使用的 Interaction Net（互動組合子）+ 平行 runtime。
這不是「另一個 ML 框架」或「另一個 Web 後端語言」。Bend 的目標是後端、需要極度可靠的 AI 生成程式碼——它年輕、Linux/macOS 表現最好，作者請大家踴躍回報 bug。
編譯速度：1 秒做完 Lean 要幾分鐘的事
Bend 的型別檢查器是 proof checker，概念跟 Lean 和 Rocq 同一掛。那些正式的證明輔助工具在中型專案跑下來要幾分鐘。Bend 宣稱最多 1 秒。
這個數字至關重要。如果是真的，AI agent 可以「每改一行就跑一次驗證」——這正是 vibe coding 需要的節奏。慢的證明器只能放在 CI 收尾階段，快的證明器可以放進 agent 的內迴圈。
為什麼這件事重要
過去五年 AI 寫 code 的痛點不是「寫不快」，而是「寫錯了很難抓」。LLM 會產出能跑的程式、能過測試的程式，但會在邊界條件、競態、邏輯繞路上偷偷埋雷。傳統解法是測試 + review，但當 AI 一晚吐出一萬行程式碼，人類根本讀不完。
Bend 的設計哲學換了一個切入點：與其 review 程式碼，不如把你不能接受的事寫成法則，讓 AI 在生成階段就被卡住。這跟「形式化驗證」(formal verification) 走的是同一條路——過去這條路太貴、太慢，沒人用得起；Bend 想讓它便宜到 agent 可以每秒跑一次。
如果這個承諾兌現，2027 年的 vibe coding 工作流會長這樣：
- 人類寫
LAWS.bend（業務不可違反的規則） - AI agent 生成實作
- 編譯器一秒內告訴 AI：「這行違反第 3 條法則，重寫」
- AI 重新生成，直到 build 通過
- 人類完全不讀程式碼也能發布
這比「AGI 自己 debug」現實得多——它把人類從「debug 工人」變成「規則制定者」。
數據解讀與質疑
- 139 分、60 則留言的 HN 表現算中等偏熱，但這是程式語言類話題的強烈訊號——這類貼文平常很難破百。
- 「速度接近 C」是 Bend 1 就在說的事，2024 年 5 月發布時就被質疑「GPU 上跑 closure 和無限制遞迴根本是浪費」。Bend 2 改走原生編譯後這個批評要重新檢驗。
- 「1 秒做完 Lean 要幾分鐘的事」這個數字需要獨立驗證。Lean 4 的社群會跳出來說「我們在特定工作流下也很快」。Siami 觀察：Bend 用了 affine dependent type theory（
BendTT論文描述的系統），簡化了 Lean 的部分表達能力以換速度——這是取捨，不是純粹優化。 - 生態系統幾乎等於零。沒有 package manager、沒有 IDE plugin（除了它自己建議寫進
AGENTS.md讓 AI 自己學）、社群不到一年。這跟 Mojo、Zig 早期很像。 - 「AI 寫 bug 被阻擋」的 demo 是刻意挑選的案例。遊戲「贏不可能」是個能用型別系統乾淨表達的不變量。真實業務邏輯的「法則」往往更模糊——能不能寫成可證明的形式，本身就是個問題。
跟同類工具的差別
| 工具 | 怎麼擋 AI 寫錯 | 速度 | 成熟度 |
|---|---|---|---|
| Bend 2 | 型別系統 + 證明（編譯期） | 宣稱 1 秒 | 年輕、預發行 |
| Lean 4 / Rocq | 互動式證明（最嚴格） | 數十秒到數分鐘 | 學術成熟、學習曲線陡 |
| TypeScript + 嚴格模式 | 型別檢查（無證明） | 毫秒級 | 生態完整 |
| 測試 + review | 執行期才抓 | 取決於測試覆蓋 | 業界標準 |
Bend 想搶的是 Lean 太慢、TypeScript 太鬆之間的那塊空地——「嚴格到能擋 AI bug、快到能放進 agent 迴圈」。這是個真實的 niche，會不會被填滿就看 2027 年的實際使用者體驗。
現在就能試
curl -fsSL https://bend-lang.com/install.sh | sh裝完只要把下面這段貼進你 AI agent 的 AGENTS.md：
When using Bend:
- run `bend guide` to learn it
- use `LAWS.bend` to keep important rules
- run `bend PROOF.bend` before committing
- parallelize the code whenever possible然後跟 agent 說「use Bend」。作者強調 Bend 適合後端、Linux、macOS——前端、嵌入式、遊戲引擎暫時不是它的戰場。
給開發者的下一步
如果你對形式化驗證有興趣但還沒入門，這條路徑最平滑：
- 先讀 Lean 4 的 Theorem Proving in Lean 4 第一章，建立「dependent type 是什麼」的概念。
- 再看 Bend 官網的 GUIDE.md（
bend guide會印出來），理解 affine dependent type 比 Lean 簡化在哪。 - 然後裝 Bend，照官方 demo 用
LAWS.bend寫一個「登入後才能存錢」的法則，讓 Claude 寫程式碼——自己親眼驗證它會被擋下來。 - 最後才決定要不要把這套工作流搬進自己的專案。
參考來源
- Bend 官網 — 主要事實來源
- GitHub: HigherOrderCo/Bend — 原始碼、issue tracking
- BendTT 論文 — 仿射依賴型理論（affine dependent type theory），Bend 的核心
- BendRT 論文 — CPU 與 GPU 平行 runtime
- Hacker News 討論串（49746163） — 139 分、60 則留言
- YouTube: Fireship 介紹 Bend — 視覺化 demo
網友熱門留言 (3)