C.M. Holt
University of Newcastle upon Tyne. 1993
One reason for the popularity of declarative languages is the reduction in distance between thinking about mathematical specifications and programming algorithms. This makes formal reasoning about programs easier; and one view holds that a programming language should be an executable subset of a specification language, so that the source and target languages of a proof are identical. A natural extension of this approach is to extend the domain of a language to include proofs; then, verification can be done entirely within the same linguistic environment. A problem that arises is the sheer size of proofs; they seem to be an order of magnitude larger than either specifications or programs. This difficulty can be mitigated by making the application of rules of inference implicit, but clear enough that a very simple-minded proof checker can derive them. The use of a visual language seems to enhance the clarity of annotations that hint at formal, explicit proofs; this is illustrated with the traditional examples of a sort and a stack.