つまり、GEN AIがたくさんのコードを生成するから、人間の価値を検証にシフトさせるってことだよね。プログラミングって本当に何なのか、時々考えるんだ。実際、英語が苦手な私にとって、プログラミングを学ぶのは大きな挑戦なんだよね。翻訳がない英語の文書を理解するためには機械翻訳に頼るしかないし、私の言語の教材は5年から6年遅れてる。今、AIが生成する何万行ものコードをレビューするのは不可能だから、数学的証明のような絶対的なルールを確立しようとする議論をよく見る。これを読むと、Rustの借用チェッカーを思い出す。実際、Rustで何度か書いた後、借用チェッカーを避けるためにトリックを使う悪い習慣に陥ることが多いんだ。数学的な厳密さが行き過ぎると、人間はそれを回避する方法を見つけがちだよね。私みたいな教育を受けていないプログラマーは特にそう。こういう試みを振り返ると、特定の形式化された答えのためだけにコードを書く結果になりそう。もしそれが標準化されちゃったら、人間のニーズに応えられるかどうかはわからない。こういう防御的なプログラミングの試みはいいと思うけど、私は攻撃的なプログラミングをしたい（この言葉は私が作った）。リスクを取るけど、すぐに修正して出荷する。時間が経てば、十分に良くなると信じてる。もちろん、精度が重要で作業範囲が明確な確立された業界、例えばJane Streetでは、この記事のアプローチは正しいと思う。つまり、市場の需要を適切にモデル化するのに十分なデータがあるから。でも、私みたいな社会的に負け組の人間が金を稼ごうとすると、常に金鉱を探してあちこち移動するから、こういう方法論は贅沢に思える。成熟したモデリングを持つ確立されたビジネスは、継続的に最適化するために高度に教育された専門家が必要なんだ。でも、現実的にはその需要についていけないってわかってる。だから、構造化されていないモデリングの場所を探してるけど、それでもこのアプローチが使えるかどうかはわからない。

前のkleppmannの投稿を見てね https://martin.kleppmann.com/2025/12/08/ai-formal-verificati...。そう、明らかに、型システムやリンターに入れられるものは、入れるべきだと思う。もっと使いやすい方法が増えるといいな。投稿に挙げられているツールの中では、dafny + irisが工業的に近いと思う。あと、amzn S3は社内でTLAを使ってた歴史があると思う。でも、この分野ではまだtypescriptを見たことがないと思う。既存のツールに落とし込めるゼロコストの抽象化で、人々が古いやり方よりも本当に好むものがあればいいんだけど。（カスタムリンターを書くのはまだまだ大変だし。golangci-lintは痛いコードベースだし、semgrepは試してないけどルールエンジンが怖そうだった。好きなAST APIはまだ使ったことがない。）

いつものことだけど、この演繹的推論への賛歌（「形式的手法」）は、その根本的な限界を見落としてる。「公理や定義が、マッピングしようとしている領域にどれだけフィットするのか？」ってことだよね。（「理論的には、理論と実践に違いはない。実践では…」）私の推測では、Jane Streetはマッピングが1:1の大きなコードベースを維持してると思う。なぜなら、そのコードの目的は決定論的アルゴリズムを実装することだから。多くの他のコーダーもそういう分野で働いてる。でも、私たちの大多数はそうじゃない。ほとんどのUIや探索的な作業など。形式的手法に並行して、高解像度で受け入れ基準を定義する動きがあるけど、論理的・数学的ではない。これは少なくともマッピング問題に取り組んでいるけど、地図が領域でないところでは解決できない。Googleの結果ページは、非常に進化した内部最適化フレームワークで本当に最適に達したのか？あなたが曖昧なアイデアを捉えるために作ったプロトタイプは、それをよりよく示すことができたのか？こういう質問は、システムの外に目を向けて、システムが何を提供しているのかを見ることで最もよく答えられる。

形式的な仕様について読むたびに、「同じテストを違う方法で書くだけ」か、もっと悪いことに「同じ実装を違う方法で書くだけ」って感じがするんだ。二度やることでエラーを見つけるのに役立つかもしれないけど、形式的な仕様がテストや実装と同じバグに悩まされるなら、何が特別なのかわからない。問題の根本は、プログラムが何かを正式に証明したいなら、その「何か」が何なのかを非常に具体的にしなきゃいけないってことだよね。そうなると、結局またテストや実装を書いてることになる。これについては何年も考えてきたけど、何かを見逃している気がするんだ。でも、それが何なのかわからない。誰か教えてくれない？