レスリー・ラモントと「あの」論文を書くために

計算、論理、数学の交差点にあるマシンロジック レスリー・ラモントと「あの」論文を書くことになった経緯 2026年8月21日 [一般型理論集合理論思い出] 人は年を取るにつれて賢くなる、あるいは少なくともそう思うようになる。そして、蓄積した知恵を若い世代に伝えることが義務となる。レスリー・ラモントは分散システムと耐故障性で名を馳せた。多くの人にとって、彼はDonald Knuthの伝説的なTeX組版システムを私たち一般人が使えるようにした有名なマクロパッケージLaTeXの著者としてよりよく知られている。レスリーは年を取るにつれて、「How to Write a Long Formula」のような一連のかなり奇抜な論文を書くことを促された。これらの論文の一つに、「Types Considered Harmful」（型は有害とみなされる）という、仕様言語における型に対する辛辣な批判があった。そのタイトルは、Edsger Dijkstraによる有名な手紙「go to文は有害とみなされる」のエコーだった。その手紙のタイトル（ジャーナル編集者によって選ばれた）は、その後多くの物事に反対する著者たちによって借用された。レスリーは型に反対していた。しかし、私はどう関わることになったのだろうか？ 型は有害とみなされる レスリーの主張は、仕様言語は型を持たない形式主義（一種の集合論）に基づくべきであり、型を持つ形式主義とは対照的であるというものだった。彼はその主張を支持するためにいくつかの議論を展開した：型を持たない形式主義はより柔軟であること、型を持つ形式主義は数多くの異常や問題を引き起こすこと、仕様における型エラーとみなされるものは検証中に anyway 検出されること。この主張にはある程度の妥当性があった。1992年にそのノートが書かれた当時、型システムは流動的な状態にあった。Coq（現Rocq）は登場したばかりで、Martin-Löfの型理論には大きな変化が起こっていた。単純型理論に関しては、HOLの初期実装が登場してからわずか数年だった。どのような型付き計算が可能になるかは不明瞭だった。証明支援系はまだ型クラスをサポートしていなかった。John Harrisonが、$T^n$を表現するのに十分うまく機能する低予算の依存型を導入するトリックを思いつくのは何年も先のことだった。その一方で、ラモントのノートは混乱していた。彼は実際の型を持つ形式主義に精通していないように見え、そのノートの大部分をストローマンを打ち倒すことに費やしていた。そこで、彼がTOPLASへの投稿を私にレフェリーとして送ってきたとき、私の評決は却下だった。もう一人のレフェリー、David McAllesterも同じ評決だった。それで終わりのはずだったが、編集者のAndrew Appelには別の考えがあった。「口紅を塗ってくれ」彼は、議論は良いことだと言った。これらのアイデアは検討される価値がある、あるいはそれに類することを言った。しかし、TOPLASに誤りを許容することはできない。なぜ私とラモントが共著者となり、論文を技術的に正確だが同じ精神のものに変えないのか？私は乗り気だった：型システムについてはかなりの知識があり、私自身の型を持たない集合論的形式主義（Isabelle/ZF）も持っており、それを宣伝できることを嬉しく思っていた。Davidも少しの間付き合ったが、すぐに手を引いた。彼は賢かった。1 レスリーと私はかなりの間論文に取り組んだ。それは不本意な共著という奇妙な形だったが、どうにかやり遂げた。新しい論文は、レスリーの主張の核心を捉えつつ、型がどのように機能するかについてのより健全な説明を含んでいた。その過程で、私はレスリーの比類なきTeXの習熟を目撃した：私がそれ以降一度も遭遇したことのない低レベルのトリック。第二ラウンドのレビュー、ああ神様Meanwhile、Andrew AppelはTOPLAS編集者を辞任していた。新しい編集者Carl Gunterは、この論文の特別なステータスについて知らされていなかった。そのため、彼の手元に届いたとき、彼はそれを新しいレフェリーに送った。これは計画の一部ではなかった。そして新しいレフェリーたちも論文を却下するという決定を下した。報告の一つは支離滅裂だった。明らかに、その著者が激昂している間に書かれたものだった。そこで私はCarlに連絡を取り、「待ってください、私の却下は無意味で、この男の却下はなぜか有効なのですか？それに、彼は文字通り狂っています。」と言った。こうして論文は結局掲載された、活発な議論を願うなどの免責事項付きで。議論が本当に起こったかどうかは定かではない。 retrospect さて、今なら27年後のレスリーの主張がどれほどうまくいっているかを問うことができる。うまくはいっていないと言うのが公平だろう。型システムは大幅に進化し、数多くの仕様および検証タスクでその価値を証明しており、その中には産業規模のものもある。CompCert検証済みCコンパイラ seL4：「世界で最も保証された、そして世界で最も高速なオペレーティングシステムカーネル」 AmazonのNitro Isolation Engine一方、集合論的形式主義を悩ませる問題については、ほとんど進歩が見られない。型がなければ、記法のオーバーロードがない。これは原理的には些細なこと（単にたくさんの異なる記号を使えばよい）だが、実際には大きな問題となる。さらに悪いことに、絶対に何でも書ける能力は、間違いを犯すための招待状に他ならない。検証は、そのような間違いを見つけるための非常に高価な方法であり、見つけられなかった間違いは、あなたの証明を無価値にする可能性がある。私の知る限り、ラモント自身の仕様言語（TLA+）さえも、最終的にはある種の型制限を設けて実装された。だから、実際には、あなたの仕様言語はおそらく型を持つべきだろう。しかし、集合論的な記法をより良く機能させる方法を探すことも依然として価値がある。彼がヒトラーカードを引く必要はなかったが。↩