The Story Behind My Collaboration with Leslie Lamport

As the years pass, people often acquire wisdom—or, at the very least, they convince themselves that they have. This perceived enlightenment usually brings a perceived obligation: the need to pass these insights down to the youth.

The Man and the Macro

Leslie Lamport is a titan in the realms of fault tolerance and distributed systems. However, to a broader audience, he is most famous as the creator of LaTeX. This essential macro package transformed Donald Knuth’s complex TeX system into something the average academic could actually use.

In his later years, Leslie developed a penchant for writing somewhat eccentric papers. Some examples include:

• "How to Write a Long Formula"
• "Types Considered Harmful"

The latter was a scathing critique of the use of types in specification languages. The title was a deliberate nod to the famous letter by Edsger Dijkstra, "go to statement considered harmful," a phrasing that became a template for countless authors wishing to denounce a specific practice.

The Great Debate: Typed vs. Untyped

Leslie's central premise was that specification languages should rely on an untyped formalism (essentially a form of set theory) rather than a typed one.

Arguments for Untyped Systems

Leslie proposed several reasons why types were a hindrance:

1. Flexibility: Untyped systems are inherently more adaptable.
2. Simplicity: Typed systems introduce various anomalies and complexities.
3. Redundancy: He argued that any "type error" in a specification would be caught during the verification phase anyway.

The State of the Art in 1992

At the time of the note's drafting, type theory was in a state of transition:

• Coq (now known as Rocq) had just debuted.
• Martin-Löf type theory was undergoing significant revisions.
• Early versions of HOL had only been available for a few years.
• John Harrison had not yet developed his method for achieving low-cost dependent types (which allows for the expression of $T^n$).

Because Leslie seemed disconnected from actual typed formalisms, his paper spent most of its time attacking "straw men."

The Peer Review Odyssey

When the paper landed on my desk at TOPLAS for refereeing, my reaction was immediate: Reject. David McAllester, the second referee, agreed.

The editor, Andrew Appel, suggested a strange compromise: Why not join Lamport as a co-author and rewrite the paper to be technically sound while keeping the original spirit?

I accepted. I was well-versed in type systems and wanted to promote my own untyped set-theoretic tool, Isabelle/ZF. It was a bizarre arrangement, but it worked. I got to see Leslie's incredible TeX skills firsthand—using low-level commands that I've never seen since.

The Second Hurdle

Disaster struck when Andrew Appel stepped down as editor. The new editor, Carl Gunter, was unaware of the paper's history. Upon reading it, he assumed the author was having a mental breakdown.

"It obviously had been written while its author was suffering a fit of apoplexy."

I had to step in and explain that my previous rejection was now void and the paper had been intentionally crafted for debate. Eventually, it was published with a disclaimer encouraging a "lively debate."

Retrospective: 27 Years Later

Looking back, how does Leslie's thesis hold up?

The Triumph of Types

Type systems have evolved massively and proven indispensable for industrial-scale verification. Examples include:

• CompCert: A verified C compiler.
• seL4: The fastest and most highly assured OS kernel.
• Amazon Nitro: The Isolation Engine.

The Failure of Set Theory

Conversely, set-theoretic formalisms still struggle with the same old problems:

• Notation: Without types, you cannot easily overload symbols. While you could just use more symbols, it is a nightmare in practice.
• Fragility: The freedom to write "anything" is essentially an invitation to introduce bugs.

Finding these bugs via verification is prohibitively expensive. If a bug slips through, the entire proof becomes worthless.

Even TLA+ (Lamport's own language) eventually incorporated some type restrictions.

Final Verdict: Your specification language should probably be typed.

However, the quest to make set-theoretic notation more efficient and usable is still a goal worth pursuing.

\text{Conclusion: } \text{Types} \approx \text{Safety} \gg \text{Untyped Chaos}