Programs from specification proofs

We present a method using an extended logical system for obtaining "correct" programs from specifications. By "correct" we mean programs that satisfy their specifications. The technique we use is to extract programs from proofs in formal logic by techniques due to Curry and Howard. The logical calculus, however, has the novel feature that as well as the conventional logical rules it includes structural rules corresponding to the standard ways of modifying specifications: renaming, exporting, signatures and enriching specifications. (We actually use a push-out construction to build sums of specifications in order to do the enriching.) Although programs extracted by the Curry-Howard process can be very cumbersome, we use a number of simplifications that ensure that the programs extracted are in a language close to a standard high-level programming language. We demonstrate the technique by showing how to implement an upper bound function in sets of partially ordered elements starting from a specification of the elements and then using sequences to implement sets before doing a final renaming.