How I came to write THAT paper with Leslie Lamport

As people grow older, they grow wiser, or at least they think they do. Then it becomes their duty to impart their accumulated wisdom to the younger generation. Leslie Lamport made his name in distributed systems and fault tolerance. For many he is better known as the author of LaTeX, the famous macro package that makes Donald Knuth’s legendary TeX typesetting system usable for the rest of us. As Leslie grew older, he felt impelled to write a series of fairly wacky papers with titles such as “How to Write a Long Formula”. Another of these papers was called “Types Considered Harmful”, a diatribe against types in specification languages. Its title was an echo of a famous letter, “go to statement considered harmful”, by Edsger Dijkstra. The title of that letter (chosen by the journal editor) was subsequently borrowed by many authors who were against lots of things. Leslie was against types. But how did I get involved? Types considered harmful Leslie‘s thesis was that specification…