AIにコードを書かせる開発は、速い。けれど、その速さが「何を作るべきか」を見誤らせることがある。Liam Powell の記事は、Bend 2 という新しい言語を題材に、その危うさをかなり具体的に示している。面白いのは、彼が単に Bend をこき下ろして終わらせていない点だ。むしろ、AIで開発を進めるときに起きやすいズレを、別の言語と実例を使って説明している。
元記事が取り上げているのは、Bend 2 が「AI coding era」のための言語として打ち出されている、という話だ。人間は「laws」と呼ばれる仕様や制約を書く。AI は実装と proof を書く。コンパイラは、その proof が正しいかを検証する。見た目にはかなり野心的で、筆者も「そういうことをしたい人がいるのは分かる」と認めている。
ただし、彼の主張は Bend そのものの思想批判ではない。問題にしているのは、Bend が vibe-coding の罠にはまっているのではないか、という点だ。vibe-coding とは、十分に調べたり設計を詰めたりする前に、LLM を使って勢いよく実装を進めてしまうやり方を指している。記事では、Bend のホームページにあるデモを例にする。そこで開発者が書く「laws」は、プレイヤーが旗に触れられず、勝てないことを示すためのものだが、それだけで 58 行ある。さらに、その laws を証明するために LLM が書く proof は 442 行にもなるという。
筆者は、ここで Bend が「単に面倒」なのではなく、もっと根本的な見落としをしていると見る。それは formal verification、つまり形式手法による検証だ。これは、プログラムが正しいことを数学的に示すための分野で、彼によれば Bend のWebサイトにもコードベースにもその言葉が出てこない。言い換えると、Bend はその分野の上に自分の言語を作っているのに、肝心の既存技術に触れずに、かなり冗長な仕組みを独自に積み上げているように見える、というわけだ。
筆者はそれを示すために、同じデモを SPARK という open source の言語・コンパイラで再現している。SPARK は formal verification 向けに作られているため、必要な条件を短く表現できる。彼は LLM に「Bend のデモを SPARK で再現して」とだけ指示し、その結果を載せている。コードでは、状態を表す record、壁を判定する関数、勝利条件を含まない安全性の invariant、そして replay の結果が勝利できず、ゴールのマスにもいないことを検証する条件が書かれている。最後に GNATprove を走らせると、「Success: all checks proved (12 checks).」と出る。筆者の言いたいことは明快で、Bend が長い proof を必要としているのに対し、既にある道具を使えばもっと短く、もっと自然に同じことができる、ということだ。
彼はここから一般論に広げる。vibe-coding は、開発者が問題を十分に理解する前に、見た目だけそれっぽい巨大な解にたどり着かせてしまう。しかも LLM は、そこに既に成熟した方法があっても自発的には教えてくれない。だから、出来上がるものが「壊れている」か「時代遅れ」かのどちらかになりやすい。Bend はその分かりやすい例だ、というのがこの記事の骨子だ。
この記事を読んでまず引っかかったのは、批判の矛先が「Bend の設計」だけではなく、「AI で作るときの学習コストの省略」に向いているところだ。Bend が formal verification の既存分野を十分に踏まえていない、という指摘はかなり強い。だが、より重要なのは、LLM を使うと「もっと良い既存解法があるかもしれない」と疑う前に、動くものが出てきてしまう点だと思う。これは速度の問題というより、探索の打ち切りの問題に近い。
しかも、ここで損をするのは完成度だけではない。開発者が自分の問題設定を言語化する機会まで削られる。SPARK の例が効いているのは、単に「同じことが短く書けた」からではない。formal verification では何を invariant として置くか、どこまでを仕様として固定し、どこからを証明に回すか、という設計のほうが本体だと見えてくるからだ。AI に任せていると、その設計の勘所より先にコード量が増える。そこが危ない。
Bend の proof が 442 行という数字は、かなり印象に残る。けれど、ここで本当に問われているのは「LLM はこんな長い証明を書けるのか」ではない。むしろ、そもそもその 442 行は誰のためにあるのか、という話だと思う。人間が読んで保守するには重い。LLM に書かせるなら、なおさら意味が薄い。しかもこの記事では、SPARK で同じ目的をかなり自然に記述できることが示されている。つまり、長い proof を量産すること自体が先進性ではない。
ここで面白いのは、AI の得意不得意よりも、道具選びの文脈がズレている点だ。もし本当に formal verification をやりたいなら、既にあるフレームワークを土台にした方がいい。逆に、LLM に「proof を書かせる」ことが目的化すると、手段のための手段を積み上げることになる。筆者はそこを「vibe-coding の罠」と呼んでいるが、私はかなり的確な表現だと思う。勢いで作ると、完成した頃には問題の本質から遠ざかっていることがある。
この記事がBend以上に刺しているのは、既存の知識への接続が抜け落ちる危険だ。LLM は質問に答えるのは上手いが、「あなたが今やろうとしていることは、実は何年も前から別の名前で研究されています」とは、文脈がなければ言ってくれない。Bend の例では、その別の名前が formal verification だった。筆者が怒っているのは、単なる言及漏れではない。分野の入り口を知らないまま、似たものを再発明してしまう構図そのものだ。
これはスタートアップにも個人開発にも起きる。AI を使うと「思いついたことをすぐ形にできる」ので、調査の順番が後回しになりやすい。だが、ソフトウェアの歴史は既存技術の上に積み上がってきた。検索、認証、静的解析、形式手法、最適化。たいていの領域には先行研究と実装がある。そこを踏まずに作ると、動いてはいるが何かが鈍いものになりやすい。この記事は、その鈍さをかなり早い段階で見抜け、と言っているように読めた。
私がこの記事を高く評価するのは、AI そのものを悪者にしていないからだ。問題は LLM ではなく、LLM を使うことで「考える前に作る」癖が強化されることにある。実装を早く始めるのは良い。しかし、何を作るべきかの地図を持たずに進めると、後から修正しづらい場所に入り込む。Bend の例は、その失敗をかなり分かりやすく見せている。
同時に、この記事には少し意地の悪さもあると思う。SPARK での再現は説得力がある一方で、比較対象がうまく選ばれすぎている面もある。Bend が目指しているのは、単なる静的検証ではなく、AI と proof を組み合わせた新しい開発体験かもしれないからだ。ただ、その可能性を認めたうえでも、既存の道具で足りる部分まで新しく作ってしまうと、開発体験はむしろ重くなる。そこはかなり現実的な警告だと思う。
