Leslie Lamportとの共著論文を書くまで：型なし形式主義の擁護論をめぐる顛末
I came to write THAT paper with Leslie Lamport
計算機科学者Lawrence C. Paulsonが、Leslie Lamportの「型は有害」という論文を査読し、却下したにもかかわらず、編集者の提案で共著者として論文を書き直すことになった経緯を振り返る。Lamportの主張は型なしの形式主義を支持するものだったが、Paulsonはその内容に問題を見出し、共著を通じて技術的に正確な形に修正した。しかし、再査読でも却下され、最終的には掲載に至るまでの紆余曲折が語られる。27年後の現在、型システムの進化によりLamportの主張は支持されにくくなっていると結論づける。
型なしで書けるということは、たいていの場合、間違いを犯すための招待状にすぎない。
HNでの議論
11- joomy
なんと、ブログ記事から最終版の論文へのリンクが貼られていない。https://www.microsoft.com/en-us/research/publication/specifi...
- srean
> もう一人の査読者、デイビッド・マカレスターも同じ結論に達した。
PACベイズ境界を導入した、あのデイビッド・マカレスターと同じ人物か？
答え：はい。
- mrkeen
> この論文には一理あった。1992年にそのメモが書かれた当時、型システムは流動的な状態にあった。Coq（現在はRocq）が登場したばかりで、マルティン＝レーフの型理論には大きな変化が起きていた。単純型理論に関して言えば、HOLの初期の実装が登場してからまだ数年しか経っていなかった。どんな型付き計算体系が何をできるのかは不明瞭だった。証明支援系はまだ型クラスをサポートしていなかった。ジョン・ハリソンが、Tnを表現するのに十分うまく機能する低コストの依存型を導入するのは、それから何年も後のことだった。
TLA+に線形型や依存型を押し込めたいわけではない。網羅的な実行時検証で動的性質を証明することは、静的に行うかもしれないこととはまったく別のゲームだ。
しかし、無意味なことを排除したいとは思う。確かに、信号機がRED_LIGHTと等しくなることはないと証明できる。だが、それがREDと等しくなったら困る。