Formality works
Formal calculations can contribute successfully to a better understanding of the structure of a proof, both in programming and in "classical" mathematics. This is illustrated by means of a few examples. (C) 2001 Elsevier Science B.V. All rights reserved.
calculational mathematics transitive closure program derivation distributed computing