Section 1.2 of Chapter 1 of Hopcroft and Ullman is concerned with procedures and algorithms. For us this is part of the basic type theory. Unlike in the case of set theory where computability need not be mentioned, in type theory computability is a basic concept. So we have covered these ideas already in section 1.
It is interesting that Hopcroft and Ullman rely on the concept of an effective procedure which is the same open-ended concept that we axiomatize in type theory. Only later, in Chapter 6, do they present Turing machines, a formalization of effective computability. Also, Hopcroft and Ullman consider the subject metamathematically. That is, they look at the mathematics from outside. For us that is like noticing properties of the underlying procedures. They do not talk about the type or the meaning of the procedures only their computational behavior. This is mathematics as influenced by the great results of logic, a new 20th century mathematics.