Bend 是一門專為「AI 幫忙寫程式」的時代設計的新程式語言，標語是打造一個「快、而且能用證明擋住 AI 錯誤」的語言。它想解決的問題是：現在很多程式碼是由 AI 代理生成或修改的，但沒有機制保證 AI 改出來的程式碼不會破壞原本該有的規則，Bend 就是想在語言層面把這件事鎖死。
Bend 最特別的功能叫 LAWS.bend,開發者可以在裡面先寫下「絕對不能違反的規則」，例如在遊戲裡宣告「沒有任何一種操作序列可以直接獲勝」，之後不管是誰(包含 AI)寫的程式碼，都必須通過數學證明才能算合格，文件裡直接寫「合併一個 bug 在數學上是不可能的，因為那是一個定理」。Bend 語法接近 Python,型別系統則是建立在類似 Lean、Rocq 的證明檢查器之上，理論基礎是仿射依賴型別論，同時支援編譯成原生機器碼，並能自動把程式碼分散到多核甚至 GPU 上平行執行。
這則消息在 Hacker News 上引發不少討論，原因是它嘗試回答一個很多工程師都在煩惱的問題：當愈來愈多程式碼由 AI 生成，要怎麼確保這些程式碼真的符合預期、不會偷偷改壞邏輯。Bend 把「證明」直接內建進語言本身，而不是事後靠測試去抓錯，是一個相對少見的做法。專案作者也坦白說這個語言「還在演進中，會有 bug」。
對還在學程式的孩子來說，Bend 目前偏技術前沿，語法背後牽涉到「證明」「型別論」這些比較進階的概念，不算是入門素材。但這則新聞很適合拿來跟孩子聊一個觀念：寫程式不只是「能跑就好」，還要想辦法證明「這段程式真的做了它該做的事」，這其實跟數學裡「證明一個定理」的精神很像。
程式語言開源AI開發工具