From Rejection to Co-Authorship: Paulson Recounts Type System Clash with Lamport

Computer scientist Lawrence Paulson recently detailed the unusual circumstances that led him to co-author a paper with Leslie Lamport, a collaboration that began with a recommendation for rejection. The account highlights a fundamental ideological divide in formal methods regarding whether specification languages should be typed or untyped.

The conflict began when Lamport submitted a note titled "Types Considered Harmful" to the journal TOPLAS. Lamport's central thesis was that specification languages should rely on untyped formalisms, such as set theory, arguing that they offer greater flexibility and that any resulting type errors could simply be detected during the verification process. However, Paulson and fellow reviewer David McAllester both recommended the paper be rejected, citing "straw man" arguments and significant technical inaccuracies.

An Unconventional Editorial Solution

Rather than issuing a flat rejection, TOPLAS editor Andrew Appel proposed a unique compromise: Paulson should join the project as a co-author. The goal was to preserve the spirit of Lamport's original thesis while transforming the manuscript into a technically accurate piece of scholarship. Paulson notes that the resulting collaboration succeeded in capturing the core of Lamport's argument while providing a "saner description of how types worked.

Despite the editorial intervention, the path to publication remained rocky. The paper faced a second round of rejection from a new set of referees, including one report that Paulson described as "incoherent" and written by someone "suffering a fit of apoplexy." The work was eventually published, though it required the inclusion of a disclaimer.

The Shift Toward Typed Safety

Looking back 27 years later, Paulson argues that Lamport's preference for untyped systems has not held up against the evidence of modern engineering. He points to the success of high-assurance projects—such as the seL4 kernel, the CompCert verified C compiler, and Amazon's Nitro Isolation Engine—as proof that typed systems are superior for managing complexity at scale.

According to Paulson, relying solely on verification to catch type errors is an "extremely expensive way to find such mistakes," warning that any errors missed during that process could render entire proofs worthless. This shift reflects a broader industry evolution toward using type systems to prevent costly mistakes before they reach the verification stage.

Future of Formal Specifications

While the debate over flexibility versus safety continues, the trajectory of the field suggests a clear preference for the safety of typed calculi. The anecdote serves as a case study in the evolution of software verification standards, moving from the theoretical flexibility of the early 1990s to the rigorous, type-driven requirements of today's critical infrastructure. This transition underscores a fundamental realization in computer science: while untyped systems offer an initial ease of expression, the long-term maintenance and correctness of critical systems demand the structural guardrails that only a robust type system can provide.