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 . 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  who showed that real, complex, and abstract analysis could be formalized in this neutral way.