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

Bend 2 とバイブコーディングの罠 2026年9月18日 [バイブコーディングに関して、Bendは私の一般的な論点を説明するための有用な例として機能します。私は、言語設計における著者の経歴について何も知りませんし、彼らが実際に以下のトレードオフを考慮して、私が貧弱な選択だと考えるものを行ったかどうかについても知りません。以下で「著者は」を、「同じものを作成できたであろう仮説上の著者は」に自由に置き換えてください。] Bend 2はAIコーディング時代のための言語として売り出されています。人間が「法則」を書き、AIが実装と証明を書き、コンパイラが証明の妥当性をチェックします。それはすべて非常に印象的に聞こえ、そのような言語を欲する人がいるのも理解できます。実際、このアイデアにはいくつかの大きな問題があります。しかし、この記事はそのことについては触れません。代わりに、Bend自体が、あまり言及されていないバイブコーディングの一般的な罠にどのように陥ってしまったかについて話したいと思います。まず、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行のコードが必要です。では、私の問題は何でしょうか？なぜこれをバイブコーディングの罠と呼ぶのでしょうか？問題は、バイブコーディングは、より良い解決策が存在することを認識するのに十分なほど問題について学ぶ前に、実質的な解決策を構築することを可能にするということです。開発者は、入門的な分野の調査で直接提示されたであろうアプローチを見逃しながら、言語全体とコンパイラを構築することができます。関係する分野は形式検証です。それらの2つの単語がBendのウェブページやそのコードベースのどこにも現れないことは注目に値します。開発者は、その分野が存在することに気づかずに、分野全体を中心に言語を構築しました。これがなぜ問題なのかを明確に実証するために、Bendがデモとして使用するのと同じプログラムを、形式検証のためのオープンソース言語およびコンパイラであるSPARKで再現してみましょう。Bendに公平を期すために、私はこれを完全にバイブコーディングしました。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の著者は、これが形式検証の分野における現在の標準であること、あるいは彼らがこの分野の存在を知っているかどうかさえ完全に無視しています。彼らは代わりに、冗長な仕様とさらに冗長な証明を必要とするこのシステム全体を考案しました。言語全体とコンパイラをバイブコーディングする前に少し調査を行っていれば、著者は何を要求すべきかを知っていたため、結果を大幅に改善できた可能性があります。この例はBendを超えて重要です。バイブコーディングは、調査を行う必要なしにすぐに結果を得ることができるため、ひどく壊れているか、現在の最先端技術から数十年遅れている設計を実装することをはるかに容易にします。LLMに関数形式的に正しいことを証明できる言語を、基本原則から証明を構築することによって尋ねると、それは喜んでそれを行います。LLMは、コンピュータがLLMなしで複雑な証明を構築でき、作業の99％を排除できることを示唆するために立ち止まることはありません。それは、あなたが構築しているものがすでにあなたが構築できる作業として大部分存在しているとは決して言いません。