AIが書いたコードを、読まずに信頼できるか — 「証明」を強制する新言語Bend 2

AIにコードを書かせる量が増えるほど、地味に重くのしかかってくる作業がある。レビューだ。

生成そのものは速い。問題はそのあと。「これ、本当に正しいの？」を人間が読んで確かめる時間が、結局ボトルネックになる。非エンジニアでも開発時間の半分以上をAIが書いたコードの読解に費やしている、という話まで出てきた2026年、この構図はもう笑い話ではない。

そこに、かなり尖った角度から答えを出してきたのが Bend 2 だ。2026年9月17日に公開され、Hacker Newsで一気に数百ポイントを集めた。作者は、interaction-combinatorランタイム「HVM」で知られるVictor Taelin。

何を解決しようとしているのか

Bendが掲げる問いは、そのまま今の開発現場の悩みを言い当てている。

AIのコードを、読まずにどうやって信頼するのか？

Bendの答えはシンプルで、そして過激だ。「AIに正しさの証明を書かせればいい」。

自然言語のプロンプトをどれだけ丁寧に書いても、AIの出力が仕様通りである保証はどこにもない。テストを書いても、テストしたケースしか守れない。Bendはそこを、コンパイラによる数学的証明で埋めにいく。

LAWS.bend という新しい発想

Bend 2の中心にあるのが LAWS.bend というファイルだ。ここに、プログラムが常に満たすべき性質を書く。

• 残高は保存される（勝手に増減しない）
• 2つのオブジェクトは決して重ならない
• ソート関数は本当に並び替える

こうした性質を、コンパイラは「証明すべき定理」として扱う。そしてコードを変更するたびに、その定理を再証明できるかをチェックする。証明が通らなければ、そのコードはコンパイルされない。

つまり「テストが通った」ではなく「破ってはいけないルールを、数学的に破れないことが確認できた」という状態でコードを固定できる。ここがBendの新しさだ。型チェッカーが、そのまま証明チェッカーを兼ねている。

AIコーディングの文脈に置き直すと、意味が見えてくる。AIにコードを書かせるとき、人間が渡すべきなのは曖昧な指示ではなく、LAWS.bend に書かれた「絶対に破れない制約」だ。AIはその制約の内側でしか動けない。レビューで人間が探すべきものが「バグ」から「制約の書き漏れ」に変わる。これは監督のコストがかなり変わる可能性がある。

GPUの上で動く関数型言語という顔

Bendのもう一つの特徴は、性能面にある。同じソースファイルを、ネイティブCPUコードにもGPUコードにもコンパイルする。強い型・純粋性・線形性のおかげで、シングルコアでは手書きのC並み、そして数千〜数万コアではそれ以上に速くなる、と主張している。

Python風の構文に依存型を載せ、C / Metal / CUDA / JavaScript に出力できる。証明チェッカーの速度についても、既存の証明支援系が数分かかるところを1秒未満で検証する、と project ページは謳う。

正直に言えば、この手の性能値やベンチマークはまだベンダー自身の主張の段階で、大規模な第三者検証が出そろっているわけではない。数字は割り引いて見ておくのが健全だ。

どこが効いてくるか

Bendがそのまま明日の業務コードを置き換える、という話ではない。依存型や形式検証は学習コストが高いし、あらゆるアプリでLAWS.bendを書けるわけでもない。

それでも、効きそうな領域ははっきりしている。金融ロジックの残高保存、ゲームやシミュレーションの衝突判定、データ構造の不変条件——「ここだけは絶対に壊れてはいけない」という核が明確な場所だ。そこにLAWS.bendで結界を張り、周辺の実装はAIに任せる。そんな分担が現実味を帯びる。

以前ストックしていた疑似コード指向のエディタ「Huzzah」も、狙いは近い。longformのプロンプトではなく、宣言的な仕様で意図をコードに刻む方向だ。AIコーディングの次の主戦場が「どう速く書くか」から「どう安全に任せるか」へ移りつつあることが、こういうツールの登場からうかがえる。

触ってみるなら

インストールはワンライナーで、ライセンスはApache-2.0。オープンソースとして誰でも試せる。詳細とソースはGitHubのHigherOrderCo/Bendにまとまっている。

現時点のBend 2は、実務投入というより「AI時代のコードの信頼をどう担保するか」という問いに対する、極めて具体的な一つの回答だ。証明を強制するという発想が正しいのか、学習コストに見合うのかは、これから使われる中で問われていく。ただ、「AIが書いたコードを読まずに信頼する」という無茶な願いに、真正面から数学で殴りかかってきた点だけは、素直に面白い。