How Euclid might have written and checked the correctness of his famous algorithm had he been a little further ahead of his time.
Leslie Lamport. Euclid Writes an Algorithm: A Fairytale. International Journal of Software and Informatics, 2011,5(1-2Part1):7~20