Leslie Lamportとの共著論文を書くまで：型なし形式主義の擁護論をめぐる顛末

I came to write THAT paper with Leslie Lamport

計算機科学者Lawrence C. Paulsonが、Leslie Lamportの「型は有害」という論文を査読し、却下したにもかかわらず、編集者の提案で共著者として論文を書き直すことになった経緯を振り返る。Lamportの主張は型なしの形式主義を支持するものだったが、Paulsonはその内容に問題を見出し、共著を通じて技術的に正確な形に修正した。しかし、再査読でも却下され、最終的には掲載に至るまでの紆余曲折が語られる。27年後の現在、型システムの進化によりLamportの主張は支持されにくくなっていると結論づける。