How I came to write THAT paper with Leslie Lamport

Lawrence Paulson recounts how he ended up co-authoring a paper with Leslie Lamport, despite initially rejecting Lamport's note "Types Considered Harmful" as a referee. The paper, which argued against types in specification languages, was eventually published after a convoluted editorial process. Paulson reflects on the debate 27 years later, concluding that type systems have proven their worth in verification, while set-theoretic formalisms have struggled.