A formal proof of this theorem is given in Table III. Like all formal proofs, it is excessively tedious, and it would be fairly easy to introduce notational conventions which would significantly shorten it. An even more powerful method of reducing the tedium of formal proofs is to derive general rules for proof construction out of the simple rules accepted as postulates. These general rules would be shown to be valid by demonstrating how every theorem proved with their assistance could equally well (if more tediously) have been proven without. Once a powerful set of supplementary rules has been developed, a “formal proof” reduces to little more than an informal indication of how a formal proof could be constructed.

C. A. R. Hoare, “An Axiomatic Basis for Computer Programming”