In his 1971 IFIP paper, Constructive Mathematics and Automatic Program Writers, Constable introduced the idea that proofs in a constructive logic could be translated into programs. Citation. He based his results on Kleene realizability for the case that the computation formalism is a high level language like Algol or a machine model such as RAM's instead of Kleene's arithmetization of mu-recursive functions. He showed that there is an extraction procedure for proofs in Intuitionistic Number Theory that makes that theory a Turing complete programming language over the natural numbers. At the same time, Bishop was suggesting a programming language called Sigma into which he could compile constructive proofs in analysis. That work was never published but was studied by a few logicians such as Nick Goodman at Buffalo at the time that John Myhill was also at Buffalo.
Constable framed his results in the context of the evolution of programming languages to "higher levels" of expressiveness and quoted from Donald Michie, editor of the book Machine Intelligence 3. In the Introduction, Michie said that the trend in language evolution was "if a passage of text is respectable mathematics in a generally accepted notation, then it will compile." This vision still motivates us as we strive for more expressive formalisms.
In subsequent work, Constable added standard imperative programs directly into the formalism of Intuitionistic Number Theory. In order to enable the realizers to be efficient code, he showed how to interpret the programs as proofs. For example, while loops and recursive procedures are interpreted as forms of inductive proof. It is immediately clear that this Algorithmic Number Theory is Turing complete. Later Dana Scott and Martin-Lof showed that the propositions-as-types principle provided higher order total functions as realizers and that one could derive the proofs-as-(higher-order-functional) programs principle from this more general principle. Citations. But their approach left open the question of translating proofs to efficient code, an issue that has continued to occupy our group since 1980 when Bates produced an implementation of these realizers in Lisp.