How I came to write THAT paper with Leslie Lamport

Lawrence C. Paulson recounts his experience co-authoring a paper with Leslie Lamport that contended against typed specification languages in favor of untyped formalism. Initially critical of Lamport's theories, Paulson details the challenges faced in the editorial process, the eventual publication of the paper, and reflects on the evolution of type systems over the years, ultimately finding that typed systems have proven their value in specification and verification tasks.