AI にコードを書かせる流れが強まるほど、「速く動く」ことと「意図どおりに動く」ことの両立が難しくなる。Bend は、その矛盾を言語設計そのものから解こうとしているプロジェクトだ。作者は、自然言語で雑に指示しても AI が実装し、しかも proof で間違いを止められる世界を見据えている。まだ若い言語ではあるが、主張はかなり野心的で、今の AI 開発ブームに真正面から乗っている。
Bend は、AI のミスを proof で塞ぐことを売りにした新しい language だ。紹介文では「a fast language that blocks AI mistakes via proof」と掲げられ、あわせて C speed、CUDA parallelism、Lean proofs、Python syntax という特徴が並ぶ。つまり、書きやすさは Python に寄せつつ、実行速度は C に近く、しかも GPU も使える。そこに proof checker を組み合わせて、AI が書いたコードが守るべき規則を機械的に確認する、という構想になっている。
サイトの冒頭では、将来の post-AGI economy では人間がコードを読んだり書いたりしなくなるかもしれないが、AI に何をしてほしいかを伝えるための曖昧さのない手段は必要だ、と説明している。Bend の答えは、自然言語の代わりに laws を書き、さらに proofs で「AI がその意図を正しく実装した」と検証することだ。単なる DSL ではなく、AI が触る前提の開発ルールを言語の中に埋め込む発想に近い。
実際の使い方としては、まずインストールし、AGENTS.md に「bend guide を読ませる」「LAWS.bend に重要なルールを書く」「コミット前に bend PROOF.bend を走らせる」「可能なら並列化する」といった指示を足す。そこまで書いたうえで、AI に “use Bend” と言えばよい、という流れだ。つまり Bend は、コードを書くための言語であると同時に、AI エージェントへの運用ルールの土台でもある。
性能面では、Bend は native code にコンパイルされ、1コアでは C にかなり近い速度で動くと主張する。さらに同じ binary が 16 コアでも GPU でも動き、1コアより最大 100 倍速くなるという。並列化は threads や locks を意識せず、仕事を二つに分ければ使える core に広げて、最後にまとめる仕組みだ。デモでは pow2.bend が GPU 上で動く様子が示されている。
安全性のデモもかなり露骨だ。LAWS.bend に「勝利に至る move sequence は存在しない」といった law を書いておくと、AI が「board を wrap around させる」新機能を入れようとしたときに、law を破る変更は merged されず、AI が retry して law を満たす実装に直さざるを得ない。サイトはこれを「Merging a bug is mathematically impossible: it is a theorem」と表現している。最後に、GUIDE.md が言語全体であり、bend guide で読めること、BendTT という affine dependent type theory と、BendRT という CPU/GPU 向け並列 runtime の paper があることも示している。
面白いのは、Bend が単に「速い新言語」を名乗っていない点だと思う。普通なら性能か書き味のどちらかを前面に出しそうだが、ここでは中心にあるのが「AI が間違える前提で、それを仕組みで止める」という考え方だ。今の開発現場で本当に困るのは、AI がコードを一応書けることではなく、細かい仕様を少しずつ外しても人間が見落としやすいことだからだ。Bend はそこを、自然言語の曖昧さではなく proof に寄せて潰そうとしている。発想としてはかなり筋が通っている。
ただし、ここで気になるのは「proof があるから安心」と言い切れるわけではないことだ。proof が守るのは、あくまで書かれた law の範囲だろう。law の定義が甘ければ、AI はその隙間を抜けるかもしれないし、逆に law を厳しくしすぎると実装の自由度が下がる。つまり、問題はバグが消えるかどうかより、どのレベルの制約を proof に落とし込めるかに移る。Bend はそこをかなり強気に押し出しているが、実運用では「何を law にするか」の設計力が重要になるはずだと思う。
Bend の説明で地味に効いているのは、Python syntax を採用している点だ。型や proof が強い言語は、どうしても学習コストの高さで敬遠されがちだが、見た目が親しみやすければ入り口は低くなる。しかも Bend は、type checker が proof checker を兼ねていて、それが Lean や Rocq に比べてかなり速いと主張する。mid-sized codebase でも minutes ではなく、最大でも 1 second 程度で確認できるというのは、AI agent が毎回差分を試す運用を想定すると確かに魅力的だ。
一方で、この設計は「人間が手で追うコード」より「AI が何度も試すコード」に向いているように見える。ここはかなり重要だと思う。人間が全部読む世界では、proof は重く感じられることがあるが、AI が書いて AI が直し、最後に機械が弾くなら、検証コストはむしろ安くなる。Bend は、その未来に賭けている。だからこそ、ターゲットは汎用言語というより、AI 支援開発のバックエンドや、ルール違反が高くつく領域に見える。Linux と macOS のバックエンドで特に向いている、と書いているのもその延長だろう。
Bend は「速い」と「正しい」を別々の機能として並べていない。native code、16 コア、GPU、CUDA parallelism、そして proof を同列に並べているのが特徴だ。ふつう並列処理は、性能を上げる代わりに複雑さが増える。ロック、スレッド、競合、データ分割……と、途端に考えることが増える。それを Bend は「no threads, no locks, no kernels to write」と切って捨て、仕事を分ければ自動で広げる、としている。ここには、並列化の面倒さを言語側に吸収してやる、という強い意思がある。
ただ、並列化は理屈がきれいでも、現実のプログラムではメモリの持ち方や副作用の扱いで詰まりやすい。だから、この主張が本当に効くのは、計算が独立しやすい領域か、あるいは言語側の制約にかなり素直に従えるコードだと思う。Bend はその点を、proof と組み合わせることでさらに攻めている。並列化しても law は壊さない、壊れそうなら止める、という姿勢だ。もしこれが実用に乗れば、性能最適化と安全性確認を別工程にしなくて済む。その意味で、Bend は「AI が速くコードを書く」ための言語というより、「AI が速くても壊せない」ようにするための言語として読むほうがしっくりくる。
サイト自体が、Bend はまだ evolving で、問題があれば issue を出してほしいとかなり率直に書いている。これは誠実でもあるし、同時に未完成さも示している。大胆な構想ほど、実際には edge case が多い。proof による安全性、GPU を含む高速実行、AI エージェントとの連携。この三つを一つの言語でまとめるのは魅力的だが、裏を返せばどこかが崩れると全体の印象が落ちやすい。だから現時点では、Bend は完成品というより「この方向に行くと開発は変わる」という提案に近い。
それでも無視しにくいのは、今のソフトウェア開発がまさにこの問題にぶつかっているからだ。AI は速いが、仕様を少しずつ壊す。人間は検証に疲れる。そこで proof と parallel runtime を一体にした Bend が出てきたのは、偶然というより時代の要請に見える。すぐに広く普及するかは分からないが、「AI の誤りを後からレビューする」のではなく、「そもそも通さない」方向へ開発を寄せる流れは、今後ほかの言語やツールにも広がっていくのではないかと思う。
参考: Bend
