Even without formalization, expressing the ideas of Hopcroft and Ullman in type theory (especially Nuprl) opens the possibility for new interpretations of their mathematics. Their definitions refer to a fragment of set theory on which they informally define algorithms and procedures, but not in a systematic way. The first thing we show is how to treat computation systematically and foundationally with minor changes in their text.
Our presentation then enables a person to imagine that all of the mathematics is classical, as Howe's work illustrates [19]. It also allows the interpretation of recursive mathematics that all functions are given by ``Turing machines'' or Lisp programs. It also allows an Intuitionistic interpretation. One way to describe this style is to relate it to the work of Bishop [3] who showed that real, complex, and abstract analysis could be formalized in this neutral way.