AIがコードを記述する未来を見据え、AIによる誤りを「証明」によって防ぐことを目的とした新しいプログラミング言語「Bend」が開発されました。
Bendは、コードの意図を正確に表現するための「法律（Laws）」と、AIがプロンプトを正しく実装したかを検証する「証明（Proofs）」の仕組みを備えています。例えば、ゲームにおいて「勝利は不可能である」という法則を定義しておけば、AIが新しいコードを生成してその法則を破るような変更を行うことを、数学的に不可能にできます。これにより、AIエージェントを用いたコーディングの信頼性を向上させることが可能です。
実行性能についても高い特性を持っています。ネイティブコードへのコンパイルにより、単一コアでC言語に近い速度を実現し、16コアやGPUを利用することで単一コアの100倍近い速度での実行が可能です。
また、コンパイル速度も極めて迅速です。型チェッカーが証明チェッカーの役割を兼ねているため、1万2800の定義を含む中規模なコードベースでも、1秒以内にコンパイルを完了させることができます。これは、LeanやRocqといった既存の言語が数分から数十秒を要するのと比較して、AIエージェントがソースコードの変更を迅速にチェックできることを意味します。
さらに、Bendはスレッドやロックを明示的に記述することなく、タスクを複数のコアに分散して効率的に並列処理を実行できる機能も備えています。