2026年9月18日 Bend は、私がバイブコーディングについて述べている一般的な点の有用な例として機能します。なぜなら、それは最近の出来事であり、高い注目を集めており、例として使いやすい側面があるからです。私は著者の言語設計における歴史について何も知りませんし、彼らが実際に以下のトレードオフを考慮し、私が悪い選択だと考える選択をしたかどうかも知りません。以下の「著者」を「同じものを作り得た仮想の著者」に置き換えても構いません。私は明らかに Bend の設計決定を気に入っておらず、それを提示したかったのですが、これが私が下で述べようとしている主な点と過度に混ざってしまっています。今これを編集して、既存のコメントが過度に厳しいように見せたくはないので、私がこの文章を書いているときの私の精神的モデルを説明するのが最善の解決策だと感じています。以下は 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 で再現しましょう。SPARK は形式検証のためのオープンソースの言語とコンパイラです。Bend に公平を期すために、私は自分自身でこれをバイブコーディングしました。つまり、私はただ LLM に SPARK でこのデモを再現するように指示し、さらなるガイダンスは与えませんでした：package Game with SPARK_Mode issubtype 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 : St...