概要
HigherOrderCoが開発する新しいプログラミング言語「Bend」(Bend 2)が注目を集めている。最大の特徴は、Python風の平易な構文を持ちながらネイティブコードにコンパイルされ、GPU上でC言語に匹敵する実行速度を発揮する点だ。加えて、型検査器に形式的証明の検証機能を統合しており、「LAWS.bend」というファイルに記述したルールに反する変更をAIコーディングエージェントが行えないよう保証する仕組みを備える。AIによる自動コード生成・自動修正が急速に広がる中、正しさをどう担保するかという課題への一つの回答として位置づけられている。
性能面の特徴
Bendはシングルコアでの実行速度がC言語に迫る水準に達しているとされ、16コアを使った並列実行では単一コア比で約100倍の高速化が確認されているという。GPU上でのベンチマークでは、記号回帰(symbolic regression)の処理がシングルコアで3.01秒かかったのに対し、GPU利用時にはわずか0.53秒で完了した。またコンパイル速度についても、12,800個の定義を含むコードベースのコンパイルが0.29秒で終わったのに対し、比較対象となったLeanでは36.2秒、Rocq(旧Coq)では5.99秒を要したと報告されており、既存の証明支援系言語と比べても際立った速さを示している。こうした性能は、スレッドロックを用いずに並列処理を可能にするアーキテクチャと、CUDA互換によるGPUへの処理分散によって実現されているという。
LAWS.bendによる形式的証明と安全性
Bendの中核的な特徴は、Leanベースの形式的証明の仕組みを型検査に組み込んでいることだ。開発者は「LAWS.bend」というファイルに、コードベースが満たすべき不変条件や制約を数学的なルールとして記述できる。例えばゲームのルールを法則として宣言しておけば、AIエージェントが新機能を追加する際に、その変更がゲームの根幹となるロジックを意図せず破壊してしまうことを型検査器が検出し、防止できるという。記事ではコミット前にbend PROOF.bendのようなコマンドを実行するようAIエージェントに指示する運用例も紹介されている。
AI時代を見据えた設計思想と今後
Bendは、人間がコードを書いたり読んだりする作業から解放される、いわゆる「ポストAGI」的なワークフローを見据えて設計されているとされる。人間による目視レビューに頼らずとも、AIエージェントが生成・変更したコードの正しさを数学的な証明によって機械的に保証できる点は、AIによる自動化が進むほど価値を増す可能性がある。現時点では「開発途上(work in progress)」であることが明言されており、バグ報告も歓迎されている段階だが、公式サイトが提供するスクリプトから容易にインストールできるという。GPUネイティブな高速実行と形式的検証を両立させるアプローチとして、AIコーディングエージェントの信頼性を高める新たな選択肢になるか注目される。