AIが書いたコードを、人間が読まずに信用できるのか。この問いに対して、新しいプログラミング言語Bendは「証明を要求する」という答えを出しました。公式サイト（bend-lang.com）はHacker Newsで注目を集めています。サイトによると、Bendは次の4つを組み合わせた言語です。
- Cに近い実行速度
- CUDAによる並列実行
- Leanのような証明
- Pythonに似た構文
守らせたいルール（law）をLAWS.bendに宣言しておくと、それを破るAIの変更は証明チェックを通らず、取り込めなくなります。AIエージェントにコードを書かせる開発が広がるなかで、この仕組みが何を保証するのかを整理します。
発表内容
公式サイトが挙げる特徴は、次の4点です。
- 実行が速い：ネイティブコードにコンパイルされ、1コアではCに近い速度で動くとされています。同じバイナリが16コアでもGPUでも動き、1コアで動かした場合と比べて最大100倍速くなるそうです。
- コンパイルが速い：型チェッカーはLeanやRocqと同じく証明チェッカーです。サイトの説明では、LeanやRocqは中規模のコードベースで数分かかることがあるのに対し、Bendは長くても1秒で終わります。このため、AIエージェントが変更のたびにチェックを回せるとしています。
- 並列化が簡単：スレッドもロックもカーネルも書く必要がありません。処理を2つに分けるだけで、Bendが使えるコアすべてに呼び出しを分散させ、最後に結果をまとめます。
- 証明でミスを止める：
LAWS.bendにlawを宣言すると、それを破るコードは出荷できなくなります。
サイトにはゲームを使ったデモがあります。「勝利は不可能」というlawを置いた状態で、Claudeに「盤面を端でつながるようにして」と頼む例です。LAWS.bendがない場合、lawを破るバグはそのままマージされました。LAWS.bendがある場合は、AIが壁を作ってlawが成り立つことを証明するまでやり直させられました。
Without LAWS.bend, the bug went live. With LAWS.bend, the AI had to retry until it built a wall and proved the law holds. Merging a bug is mathematically impossible: it is a theorem.
lawの記述例として、サイトには次のコードが載っています。
# LAW: no move sequence leads to victory.
law you_cant_win :
for moves: List<Move> # any sequence of moves
board = replay(start(), moves) # replayed from the start
is_won(board) == False {} # never leads to victoryこのlawの証明はPROOF.bendに置き、AIが書きます。サイトはLAWS.bendを「証明の裏付けがあるAGENTS.md」と説明しています。
導入手順は2ステップです。まずインストールスクリプトを実行し、次にAGENTS.mdへ以下を追記します。あとはエージェントに「use Bend」と伝えるだけ、という流れです。
curl -fsSL https://bend-lang.com/install.sh | shWhen 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なぜ重要か
公式サイトは、Bendを作った問題意識を次のように説明しています。
In the post-AGI economy, humans will eventually stop writing and reading code, but we still need an ambiguity-free way to tell the AIs building the world around us what we want done.
AGENTS.mdのような自然言語の指示は、AIが読み飛ばすことも、誤解することもあります。Bendはその指示の一部をlawという形で書かせ、守られているかを型チェックで確かめます。サイトの言い方では、「Make no mistakes」が型チェックされるようになります。チェックが1秒以内で終わるなら、エージェントのループに毎回組み込めます。そうなれば「AIに書かせる」工程と「証明で確かめる」工程をひとつの流れにできる、というのがこの言語の狙いです。
現時点での未確定事項
- ベンチマークの数値：Apple M4 Maxで計測したグラフがあると書かれていますが、取得したテキストには具体的な数値や比較条件が入っていませんでした。
- 対応環境：サイトには「バックエンド、Linux、macOSで最もよく動く」とだけ書かれています。Windowsへの対応や、NVIDIA以外のGPUで動くかどうかは書かれていません。
- 「バグフリー」の範囲：証明で守られるのは、
LAWS.bendに宣言したlawだけです。宣言していない性質も保証されるのかどうか、サイトは説明していません。 - 成熟度：サイト自身が「Bend is young」「Expect bugs」と書いており、まだ開発途上です。ライセンスや安定版のリリース時期は書かれていません。
理論の詳細は、GUIDE.mdと2本の論文で説明されています。BendTTはBendの核となるアフィン依存型理論で、BendRTはCPUとGPUで動く並列ランタイム（VM）です。
まとめ
- Bendは、
LAWS.bendに宣言したルールをAIが破れないよう、証明チェックで強制する言語です。 - 公式サイトは、C並みの1コア性能、CPU/GPUでの自動並列化、1秒以内の型チェックをうたっています。
- ベンチマークの数値、Windows対応、保証の範囲は、まだ元記事から確認できません。
実装家として見ると、Bendの価値は「バグがゼロになること」ではありません。絶対に壊したくない性質を、人間が数行のlawとして固定できることにあります。証明が保証するのは「lawが守られていること」までで、lawそのものが正しいかどうかは人間の責任として残ります。現場で試すなら、全部をBendで書く必要はないと思います。課金ロジックや状態遷移のように壊れると痛い部分をバックエンドから選び、lawを書いてエージェントに証明させるのが現実的な入り方です。まずはbend guideで言語を確かめるところから始めるつもりです。インストールがcurlでスクリプトを直接実行する形式なので、中身を確認してから実行することもおすすめします。
コメント