On the desirability of mechanizing calculational proofs

Dijkstra argues that calculational proofs are preferable to traditional pic torial and/or verbal proofs. First, due to the calculational proof format, incorrect. proofs are less likely. Second, syntactic considerations (lettin g the "symbols do the work") have led to an impressive array of techniques for elegant proof construction. However, calculational proofs are not forma l and are not flawless. Why not make them formal and check them mechanicall y? (C) 2001 Elsevier Science B.V. All rights reserved.