Bend 2 とバイブコーディングの罠

Bend 2 と Vibe-Coding の罠

2026年9月18日

Bendは、最近の注目度の高さと例として使いやすい側面から、Vibe-Codingに関する私の一般的な見解を示すのに役立つ例として機能します。私は、言語設計における著者の過去の経験について何も知りませんし、彼らが実際に以下のトレードオフを検討し、私が貧弱な選択だと考えるものを行ったかどうかはわかりません。以下の「著者」を、「同じものを作成できたであろう架空の著者」に置き換えていただいても構いません。

私は明らかにBendのデザイン上の決定を気に入っておらず、それらを提示したかったのですが、それは以下の私の主な論点と過度に混同されています。今これを編集して、既存のコメントが過度に厳しく見えるようにしたくありませんので、執筆中に記事が私の頭の中でどのように見えていたかを説明することが最善の解決策だと感じています。

Bendの著者によるコメントはこちらです。

Bend 2は、AIコーディング時代のための言語として売り出されています。人間が「法則」を書き、AIが実装と証明を書き、コンパイラが証明の妥当性をチェックします。それはすべて非常に印象的に聞こえ、なぜ誰かがそのような言語を欲しがるのか理解できます。このアイデアには実際にはいくつかの大きな問題がありますが、この記事はそのことについてではありません。代わりに、Bend自体が、あまり言及されていないVibe-Codingの一般的な罠にどのように陥っているかについて話したいと思います。

Bendがホームページのデモで開発者に書かせることの基準から始めましょう。

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

コードはそれほど重要ではないため、ここでは再現しません。この記事にとって重要なのは、それがかなりの量のコードであるということです。プレイヤーが決してフラグに触れたりゲームに勝ったりできないと述べるだけで、58行のコードが必要です。LLMがこのプログラムのコードを書く際に、その「法則」を証明するために書く必要があるものを見てみましょう。

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

それは大量です。これらの単純なプロパティを証明するために442行のコードが必要です。

では、私の問題は何でしょうか？なぜこれをVibe-Codingの罠と呼ぶのでしょうか？

Vibe-Codingの問題は、開発者が問題について十分に認識する前に、はるかに優れた解決策が存在することを認識する前に、実質的なソリューションを構築できることです。開発者は、入門的な調査で直接提示されるであろうアプローチを見逃しながら、言語全体とコンパイラを生成できます。

問題となっている分野は形式検証です。それらの2つの単語がBendのウェブページやコードベースのどこにも現れないことは注目に値します。開発者は、その分野が存在することに気づかずに、分野全体を中心に言語を構築しました。

これがなぜ問題なのかを明確に実証するために、Bendがデモとして使用しているのと同じプログラムを、形式検証のためのオープンソース言語およびコンパイラであるSPARKで再現してみましょう。Bendに公平を期すために、私はこれを完全にVibe-Codingしました。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-Codingで言語とコンパイラ全体を構築する前に少し調査を行っていれば、結果を大幅に改善できたはずです。なぜなら、著者は何を求めるべきかを知っていたからです。

この例はBendを超えて重要です。Vibe-Codingは、十分な調査を行うことなくすぐに結果を得ることができるため、ひどく壊れているか、現在の技術水準から数十年遅れている設計を実装することを非常に容易にします。LLMに、基本原則から証明を構築することによって関数の形式的な正しさを証明できる言語を要求すると、LLMは喜んでそれを行います。LLMは、コンピュータがLLMなしで複雑な証明を構築でき、作業の99％を排除できることを示唆するために立ち止まることはありません。LLMは、あなたが構築しているものがすでに構築できる作業として大部分存在することを決して教えてくれません。