The Hoare calculus is meant to be used on practical programs such as programs that search or sort arrays, calculate number theoretic functions, play games or that use clever tricks to implement an algorithm efficiently. Given a specification and a nontrivial algorithm, a paper and pencil verification of the corresponding program using the Hoare rules may present a formidable task. Typically, early versions of the program contain bugs, first attempts at formulating an invariant for a while-loop are incorrect, leading to a new proof attempt for every small correction. Each backwards proof attempt in turn produces a plethora of logical expressions, so called ``verification conditions'' that have to be shown valid in the data structure. For this reason, it is absolutely necessary, to have some machine support, if the calculus is to be useful.
In a somewhat weaker sense the same holds true in the teaching of program- verification. It is very hard to go beyond some very trivial examples because of the sheer number of verification conditions that are freshly generated with each proof attempt.