On a nonconstructive type theory and program derivation

Jan M. Smith

pp. 331-340

in: Dimiter G. Skordev (ed), Mathematical logic and its applications, Berlin, Springer, 1987

Abstract

Not considering philosophical arguments, the main motive for using constructive reasoning when constructing programs is that constructive proofs have computational content. For instance, formulating a specification and proving it in Martin-Löf's type theory, gives a program satisfying the specification. On the other hand, extracting programs from classical proofs is in general not possible. However, the process of deriving a program may not only involve the actual construction of the program but also the verification that an already constructed part of the program satisfies some property and it is then quite possible to use classical logic. A system for program derivation where you may use classical logic is the one developed by Manna and Waldinger [5].