Euclid Writes an Algorithm: A Fairytale
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.