Identifying the informal concept of effective calculability with a rigorous mathematical notion like general recursiveness or Turing computability is still viewed as problematic, and rightly so. In a 1934 conversation with Church, Gödel suggested finding axioms for the notion of effective calculability and “doing something on that basis” instead of identifying effective calculability with λ-definability; that identification he found “thoroughly unsatisfactory”. He introduced in his contemporaneous Princeton lectures (Gödel 1934) the class of general recursive functions through the equational calculus, but was not convinced at the time that this mathematical notion encompassed all effectively calculable functions. (See (Davis 1982) and (Sieg 1997).)