 These developments will be surveyed in  Section 3.  As we will see there, an important theme in the early stages of computability theory was the characterization of a notion of effective computability which is capable of supporting rigorous proofs grounded in intuitions about algorithmic calculability but which abstracts away from the details of the models mentioned in  Section 1.6.  To this end, Gödel’s original definition of the general recursive equations was replaced in early textbook treatments (e.g., Shoenfield 1967, Rogers 1987) by Kleene’s definition of the partial recursive functions in terms of the unbounded minimization operator introduced in  Section 2.2.  This characterization has in turn been replaced by machine-based characterizations such as those of Turing (1937) or Shepherdson &amp; Sturgis (1963) in later textbooks (e.g., Soare 1987, Cutland 1980) which are closer in form to informally described computer programs.