Author recounts collaboration with Leslie Lamport on "Types Considered Harmful" paper

The Genesis of a Controversial Paper

The article recounts the background of a paper titled "Types Considered Harmful," co-authored with Leslie Lamport. Lamport, known for his work in distributed systems and LaTeX, developed a series of unconventional papers, including this one, which echoed Edsger Dijkstra's "go to statement considered harmful" by criticizing types in specification languages.

Lamport's Argument Against Types

Lamport's central thesis proposed that specification languages should utilize untyped formalisms, specifically a form of set theory, rather than typed ones. He argued that untyped systems offered greater flexibility, that typed formalisms presented numerous anomalies, and that type errors in specifications would be detected during the verification process regardless.

Context of Type Systems in 1992

The author notes that in 1992, when Lamport's initial note was written, type systems were undergoing significant changes. Coq had recently emerged, Martin-Löf type theory was evolving, and early implementations of HOL were new. The capabilities of typed calculi were not yet fully established, and proof assistants lacked features like type classes, which would later be developed.

Initial Refereeing and Collaboration

Upon receiving Lamport's note for refereeing for TOPLAS, the author, along with another referee, David McAllester, recommended rejection, citing Lamport's apparent unfamiliarity with actual typed formalisms and his focus on "straw men." However, the editor, Andrew Appel, encouraged the airing of these ideas, leading to the author's involvement in the paper's development.