型検査は通り、フォーマッタは黙っていた

AI が構文的に正しいコードを数百行すぐ出せるようになったので、生産性の律速は書く速さではなく、 レビューと検証の速さになった。この診断は正しいと思う。そして処方はたいてい言語機能で書かれる — 静的型が幻覚を弾き、フォーマッタが揺れを消し、速いコンパイルが自己修正ループを回し、厚い標準 ライブラリが怪しい依存を減らす。最後の防衛線として「人間が速く読めるコード」が置かれる。

私はこの一週間、Mere という自作言語のコンパイラを v0.1.263 から v0.1.273 まで進めていた。5 つの バックエンド（インタプリタ・C・LLVM・Wasm・RV32I）を持つ処理系で、文字列の表現を移行し、失敗の 意味を揃え、末尾呼び出しを直していた。診断が正しいなら、その一週間の記録は処方の効き目についても 何か言えるはずだった。数えてみたら、誤りを実際に捕まえたものは一つも言語の中に無かった。

以下は Mere の宣伝ではない。5 実装を持つ処理系はこの種の記録を取りやすいという、ただそれだけの 理由で証拠として使う。

一週間分の表

何が起きていたか	静的型	フォーマッタ	人間が読む	実際に捕まえたもの
self-host したバックエンドが、古い文字列表現のまま同じ ABI 番号を名乗る	通る	黙る	三日通った	4 実装に同じ値を印字させる差分テスト
nan < 0.0 がインタプリタだけ true	通る	黙る	見えない	書けるようになった値で書いた新しいゲート
「キーが無い」が 3 つのコンパイル系で catch できない	通る	黙る	見えない	コレクションの値域ゲート
str_repeat s 0 が LLVM だけ長さ欄なしで確保する	通る	黙る	見えない	文字列の値域ゲート
list_filter だけが末尾再帰でない	通る	黙る	見えない	10 万要素を流したゲート、次に grep
スタック溢れに名前が無く、2 実装が無言で死ぬ	対象外	対象外	死因が出ない	失敗プログラムを並べたゲート
ゲートが三日前のバイナリを検査していた	—	—	「コードが悪い」と誤読した	CI と手元の環境差を疑ったこと
もう真実でない pin がディスクに残り続ける	対象外	対象外	気づかない	pin の失効自体を失敗にしたこと

三列目が一件も捕まえていない。処方の最後の防衛線がそこなので、これは小さい話ではない。

ガードレールは一つのプログラムを守り、ゲートは問いを守る

なぜこうなるかは、守っている対象が違うからだ。型検査もフォーマッタも、いま手元にある一つの プログラムの内部整合を見る。表現が首尾一貫しているか、名前が解決するか、書式が揃っているか。 どれも「このプログラムは、それ自身と矛盾していないか」という問いだ。

上の表の行は、どれもその問いに対して健全だった。番号を名乗るコードは型が合っている。nan の 比較は型が合っている。三日前のバイナリを検査するシェルスクリプトは、それ自体としては正しく 動いていた。矛盾は一つのプログラムの中ではなく、二つのものの間にあった — 二つの実装の間、 宣言と実装の間、検査するものと検査されるものの間。

一つのプログラムの中を見る道具は、原理的にそこに届かない。

三件だけ中を見る。

ABI 番号は宣言であって検査ではない。 この処理系は Wasm モジュールと JS ホストの間の表現を ABI 番号で約束している。文字列は「長さ 4 バイト、本体、NUL」で、値は本体の先頭を指す。ところが モジュールを作るコンパイラは二つある（OCaml 実装と、自分自身でコンパイルした self-host 版）。 self-host 版だけが長さ欄を持たない古い表現のままで、それでいて同じ番号を stamp していた。 長さ欄を信じたホストは、一つの文字列に対して 567KB の NUL を印字した。番号が一致することは、 実装が一致することを意味しない。同じ番号を名乗る実装が二つ以上あるなら、番号ではなく 振る舞いを突き合わせる検査が要る。捕まえたのは、4 実装に同じ文字列を印字させるテストだった。

ゲートは検査対象そのものをキャッシュしてはいけない。 self-host の検査スクリプトが 7 件全滅した。 コンパイラは壊れていなかった。スクリプトは self-host コンパイラを /tmp に建てるのだが、 「ファイルが無ければ建てる」だった。そこにあったのは三日前、ABI を変える前のバイナリで、 ゲートは誰も訊いていないコンパイラを検査していた。入力やオラクルや vendoring したデータを キャッシュするのは正しい。被験体をキャッシュすると、ゲートは別のものを検査する。

この嘘には厄介な形がある。壊れているという顔で出る。 無言の緑ではなく赤なので、 「ゲートが赤い、ならコードが悪い」という当然の推論が働いてしまう。しかも CI は一度も 反対しなかった。CI のランナーは /tmp が空なので毎回新しく建てて、常に緑だった。 同じコミットが、誰も見ていない機械では緑、作業している機械では赤で、赤の方が間違っていた。 毎回建てても 260 ミリ秒で、キャッシュする理由は最初から無かった。

ゲートには「もう違反していない」も検出させる。 この処理系には、直せない差分をテストから 外さずに固定しておく仕組みがある。ある実装だけ答えが違うとき、その差分を宣言として書き留めて おく。ところがその差分が一致し始めたとき、テストは黙って通していた — 一致したケースは 宣言を読まないからだ。つまり「もう真実でない宣言」がディスクに残り続ける形になっていて、 これはこの仕組みが防ぐはずのものそのものだった。失効した宣言を失敗にしたら、その週の作業が 終わったことを教えてくれたのは、その新しい失敗だった。違反の検出だけでは、直したことが 記録から消えない。

「人間が読める」列について

可読性が無価値だという話ではない。上の修正はどれも、読める言語で書かれていなければ できなかった。だが「AI が書き、人間が検証する」という工程の像は、この一週間の実態と 合っていなかった。実際に起きていたのは、機械が検証し、人間の仕事は訊く問いを設計すること だった。

そう考えると、この週に得た規則が全部「問いの設計」の話だったことに説明がつく。ゲートは 検査対象をキャッシュしない。ゲートは検査した件数を言う（0 件は「走らなかった」と区別が 付かない）。オラクルにはバージョンがあるので固定して、何と比較したかを印字する。訊かない ことで一致させない。数字は二つ持つ（一方が動かないときに他方が動くことがある）。依存不在の skip と本物の失敗の skip を分ける。どれ一つとして可読性の話ではない。

証明はどうか

ここまで「ガードレール」と呼んできたのは型検査とフォーマッタのことだった。だがそれは この議論の一番強い形ではない。MoonBit は 0.9 で形式検証を言語の一級要素にした — contract、述語、ループ不変条件、proof_assert が構文であり、コンパイラがそれを直接 理解する。狙いは明示的に AI 向けで、生成されたコードが動くだけでなく正しいと証明できる ことを目指している。これは型検査よりずっと遠くまで届くし、上の二分法はそれを取りこぼしている。

取りこぼしを埋めたうえで、それでも結論は変わらないと思う。証明とゲートは違う壊れ方をする からだ。

証明が答えるのは「実装は仕様を満たすか」で、その仕様は人間が書いたものだ。上の表の行を 見直すと、どれも違反された主張を誰も書いていなかったケースだった。

• ABI 番号は仕様そのものだった。文字列は「長さ 4 バイト、本体、NUL」だと書いてある。 壊れていたのは実装と仕様の関係ではなく、同じ仕様を名乗る実装が二つあって、片方が 別のものだったこと。どちらの実装も、自分自身については何も嘘をついていない
• 三日前のバイナリを検査していたゲートは、検査対象について正しい仕様を持っていても 救われない。間違ったコンパイラの方が仕様を満たしていたからだ。問われていたのは 「正しく検査したか」ではなく「何を検査したか」だった
• 失効した pin は、もう真実でない仕様そのものだった。実装を仕様に照らす仕組みは、 仕様の方が古びたことを教えてくれない

ゲートにも固有の壊れ方があり、それは次の節に書く。

どちらかがもう一方を含むという話ではない。証明は仕様の質で上限が決まり、ゲートは 比べているものの独立性で上限が決まる。 そして証明だけが届く範囲は実際にある。境界条件や 不変条件のように契約として書ける種類のバグについては、形式検証は私が持っているものより 厳密に強い。ゲートがたまたま訊いた入力ではなく、すべての入力について答えるからだ。 上の表の str_repeat s 0 はその側にある — 「結果は常に妥当な長さ欄を持つ」と書いてあれば、 誰も 0 を試そうと思いつかなくても捕まった。

これで主張は有益に狭まる。「答えは言語の外にある」ではなく、この一週間で効いたものは 全部言語の外にあり、そのいくらかに届きえた言語側の仕組みは、型ではなく証明だった、だ。

二つの限界

この主張には限界があり、片方はこの週に自分で噛んだものだ。

一致が証拠になるのは、一致しているものが独立なときだけ。 少し前に、メモリから 32 ビットを ビッグエンディアンで読む関数が符号拡張するバグを直した。不透明な画素は alpha が 0xFF なので、 画素を扱うプログラムは全部これを踏む。ところがこのバグは 5 実装の差分テストでは捕まらなかった。 JS ホストも同一のバグを持っていたからだ（getInt32 を使っていた）。複数実装を突き合わせる 検査は型検査より射程が広いが、無敵ではない。独立性が成り立つ範囲でしか効かない。これを 言わずに「差分テストが守ってくれる」と書くのは、「型検査が守ってくれる」と同じ種類の言い過ぎだ。

そしてこれは一人・一プロジェクト・一週間分の記録でしかない。 表の 8 行は具体的で日付が あるが、8 行は 8 行だ。ここから「言語機能は検証に効かない」を導くことはできない。導けるのは もっと狭いことで、少なくともこの一週間、効いたのは全部言語の外にあった、という一つの 反例にとどまる。

言語設計への含意があるとすれば

「ガードレールを増やせ」ではないと思う。ゲートを置ける形にせよ、だ。具体的には三つある。

一つ、同じ問いを独立に答えられる先を複数持てること。この処理系がこの週に見つけた欠陥の 大半は、5 実装に同じ問いを訊いたから出た。単一実装の言語はこの検査を原理的に持てない。 外部の規範コーパスや別実装との差分でも代替はできるが、それは言語の外に用意しなければ ならないものになる。

二つ、「何が存在するか」をコンパイラに訊けること。この処理系は以前、どのバックエンドに どの組み込み関数があるかを手書きの表で持っていて、三つある表が三つとも古びていた。信用 できない表は表が無いより悪い。いまはコンパイラに問い合わせて表を生成し、毎回差分を取る。 AI が古びたドキュメントを読んで嘘を書く問題に対して、ドキュメントを自動更新するのではなく、 ドキュメントを生成物にするという答え方がある。

三つ、失敗の表面が揃っていること。同じ失敗がバックエンドごとに違う名前を持つと、 検査はその違いを本物の差だと報告する。この週に「一番よく起きる失敗が一番名前が無い」形を 見つけた。この処理系のプログラムが実際に死ぬ最頻の形はスタック溢れなのに、それは言語が 何も言わない唯一の失敗で、二つの実装は無言で終了コード 139 を返すだけだった。珍しい失敗 （ゼロ除算、キー欠落）から順に名前を付けていくと、最頻の失敗だけが「言語の外側の出来事」 として残る。

三つとも、生成されたコードを読みやすくする話ではない。機械が問いを持ち続けられるように する話だ。検証がボトルネックだという診断が正しいなら、投資先はそちらにある。