How I came to write that paper with Leslie Lamport

Leslie Lamport, known for distributed systems and LaTeX, wrote a series of unconventional papers, including "Types Considered Harmful," a critique of typed formalisms in specification languages that echoed Dijkstra's famous title. Lamport argued for untyped set-theoretic formalisms, claiming they were more flexible, that typed formalisms created anomalies and issues, and that type errors would be caught during verification anyway. In 1992, however, type systems were in flux: Coq had just appeared, Martin-Löf type theory was changing, simple HOL implementations were only a couple of years old, and dependent types were not yet widely supported, so there was some merit to the critique.

Despite this, the note was technically messy and attacked straw men. The author, acting as a referee, rejected the paper, as did the other referee, David McAllester. The editor, Andrew Appel, suggested that instead of rejecting outright, the author should team up with Lamport to rewrite the paper into something technically accurate while preserving its spirit. The author, familiar with type systems and promoter of his own untyped Isabelle/ZF formalization, agreed; McAllester dropped out early. After working together for some time, they produced a paper that captured the core of Lamport's argument in a correct form.