Euclid Writes an Algorithm: A Fairytale

Leslie Lamport

International Journal of Software and Informatics 5, 1-2 (2011) | , Vol 1

This was an invited paper for a festschrift in honor of Manfred Broy’s 60th birthday. It’s a whimsical introduction to TLA+, including proofs. Judged as literature, it’s probably the best thing I have ever written.