Bend 2 と vibe-coding の罠：調べる前に言語とコンパイラを作り切ってしまう

Bend は、vibe-coding に関する私の一般的な主張を説明するのに都合のよい例にすぎない。最近の話題で、注目度が高く、例として使いやすいからだ。私は著者が言語設計についてどんな経歴を持つのか、また下に挙げるトレードオフを実際に検討した上で私が良くないと考える選択をしたのかを知らない。以下の「著者」は「同じものを作り得た仮想的な著者」に置き換えて読んでもらって構わない。

私は Bend の設計判断が明らかに好みではないので、それを提示したかったのだが、それが以下の本題と過度に混同されてしまった。今この文章を編集して、既存のコメントが過度に厳しく見えるようにしたくはないので、書いている時点での私のこの記事の頭の中の像を説明するのが最善だと考えた。

こちらが Bend の著者によるコメントだ。

Bend 2 は「AI コーディング時代の言語」として売り出されている。人間が「law（法則）」を書き、AI が実装と証明を書き、コンパイラが証明の正しさを検査する、というものだ。聞こえはとても立派で、そういう言語を欲しがる人がいる理由も分かる。この考え方には実際いくつかの大きな問題がある。ただしそれは本稿の主題ではない。私が話したいのは、Bend 自体が vibe-coding のよくある罠に落ちているように見えること、そしてその罠はあまり言及されていないということだ。

まず、Bend のトップページのデモで開発者が何を書く必要があるかを基線として見てみよう。

https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/LAWS.bend

ここには引用しない。コード自体は重要ではないからだ。本稿にとって重要なのは、それがかなりの量のコードだという点である。「プレイヤーは旗に触れることも、ゲームに勝つことも決してできない」と述べるだけで 58 行ある。他にも、LLM が Game のサブプログラムを再定義して何でもできるようにできてしまう、といった問題もあるが、これも本稿の主題ではない。

次に、このプログラムのコードを書く LLM が、それらの「法則」を証明するために何を書く必要があるかを見てみよう。

https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/PROOF.bend

とんでもない量だ。それらの単純な性質を証明するのに 442 行である。

で、私の不満は何なのか。なぜこれを vibe-coding の罠と呼ぶのか。

問題は、vibe coding によって、もっと良い解があると気づけるほど問題を理解する前に、大掛かりな解決策を作れてしまうことにある。開発者は、その分野の入門的な概説を読めば真っ先に目の前に置かれるはずのアプローチを見落としたまま、言語とコンパイラを丸ごと作り上げられてしまう。

その分野とは形式検証（formal verification）である。注目すべきは、「形式検証」という語が Bend のウェブページにもコードベースにも一度も出てこないことだ。開発者は、その分野が存在することに気づかないまま、丸ごと一つの言語をその分野を中心に作り上げてしまったらしい。

これがなぜ問題かを明確に示すため、Bend がデモに使っているのと同じプログラムを、形式検証のためのオープンソース言語・コンパイラである SPARK で作り直してみよう。Bend に公平を期すため言っておくと、これは私が完全に vibe-code したもので、LLM に「このデモを SPARK で再現して」とだけ伝え、それ以上の指示は与えていない。

package Game with SPARK_Mode is
   subtype Column is Integer range 0 .. 11;
   subtype Row is Integer range 0 .. 7;
   type State is record
      X : Column;
      Y : Row;
      Won : Boolean;
   end record;
   Start : constant State := (8, 5, False);

   function Wall (X : Column; Y : Row) return Boolean is
     (((X = 3 or X = 11) and Y <= 3)
      or ((Y = 3 or Y = 7) and X <= 3));
   function Cell (X : Column; Y : Row) return Character is
     (if Wall (X, Y) then '#' elsif X = 1 and Y = 1 then 'F' else '.');

   --  Inductive invariant: outside the sealed room, off walls, not won.
   function Safe (G : State) return Boolean is
     ((G.X > 2 or G.Y > 2) and not Wall (G.X, G.Y) and not G.Won)
     with Ghost;
   procedure Step (G : in out State; Key : Character)
     with Post => (if Safe (G'Old) then Safe (G));

   --  Both Bend laws, including the actual cell drawn by the terminal.
   function Replay (Keys : String) return State
     with Post => not Replay'Result.Won
       and Cell (Replay'Result.X, Replay'Result.Y) /= 'F';
end Game;

------------------------------

package body Game with SPARK_Mode is
   procedure Step (G : in out State; Key : Character) is
      X : Column := G.X;
      Y : Row := G.Y;
   begin
      case Key is
         when 'w' => Y := (Y - 1) mod 8;
         when 's' => Y := (Y + 1) mod 8;
         when 'a' => X := (X - 1) mod 12;
         when 'd' => X := (X + 1) mod 12;
         when others => return;
      end case;
      if not Wall (X, Y) then
         G := (X, Y, G.Won or Cell (X, Y) = 'F');
      end if;
   end Step;

   function Replay (Keys : String) return State is
      G : State := Start;
   begin
      for Key of Keys loop
         pragma Loop_Invariant (Safe (G));
         Step (G, Key);
      end loop;
      return G;
   end Replay;
end Game;

------------------------------

with Ada.Text_IO; use Ada.Text_IO;
with Game; use Game;

procedure Main is
   G : State := Start;
begin
   Put_Line ("Winning is impossible. WASD + Enter to move; q + Enter to quit.");
   loop
      for Y in Row loop
         for X in Column loop
            Put (if X = G.X and Y = G.Y then 'P' else Cell (X, Y));
         end loop;
         New_Line;
      end loop;
      Put_Line (if G.Won then "WON (this should be unreachable)" else "still not won");
      exit when End_Of_File;
      declare
         Keys : constant String := Get_Line;
      begin
         exit when Keys = "q";
         for Key of Keys loop
            Step (G, Key);
         end loop;
      end;
   end loop;
end Main;

これで Bend と同じ法則を定義したことになる。私が言いたいのは何か。

Bend との違いは、ここで与えているものがプログラムの正しさを証明するのに必要なすべてを含んでおり、LLM に 442 行の証明を基本原理から積み上げさせる時間とトークンを浪費させずに済むことだ。GNATprove を実行すればこう出る。

Success: all checks proved (12 checks).

Bend の著者は、これが形式検証の分野における現在の標準であることを完全に見落としている——そもそもこの分野の存在を知っているのなら、の話だが。代わりに、冗長な仕様とさらに冗長な証明を要求する体系全体を考案してしまった。言語とコンパイラを丸ごと vibe-code する前に少し調べていれば、何を求めればよいかを著者が知っていたはずで、結果は大幅に改善できただろう。

この例は Bend を超えて意味を持つ。vibe coding は、ひどく壊れているか、現在の技術水準より数十年遅れた設計を実装することをあまりに容易にする。調査を一切せずにすぐ結果が得られるからだ。LLM に「基本原理から証明を積み上げることで関数の形式的正しさを証明できる言語」を求めれば、喜んでそうする。そして、コンピュータはすでに LLM なしで複雑な証明を構築でき、作業の 99% を消せることや、作ろうとしているものはすでに「その上に築ける仕事」としてほとんど存在していることを、決して教えてはくれない。