In order to turn the intuitive concepts discussed in the previous article into exact concepts, one would have to define exactly what a program is. Different mathematicians (including Alan Turing, Alonzo Church, Stephen Cole Kleene and others) have come up with different formalisms in order to define exactly what a computable function is and thus what a program or “algorithm” is. The different formalisms (which may be thought of as simple programming languages, although some of them where designed before actual computers where built) have turned out to be equivalent, i.e they describe the same set of functions. It was possible to prove that the exact formulizations of the above mentioned concepts as “Turing-computable functions”, “general recursive functions” etc. described the same set of functions although the formalisms are very different. It is possible to translate from one of these formal languages into the other and vice versa. Likewise, “turing-enumerable” sets and “recursively enumerable sets” are the same, etc. A number of more recent such formalizations of the concept of computability, like “register machines” or “while-programs”, for example, are more similar to the way actual computers or actual programming languages are designed. In each case, the equivalence to the earlier, more mathematical formalisms, like “Turing machines”, “lambda calculus”, “recursive functions”, etc. could be demonstrated.
This lead to the hypothesis that every function that is computable is recursive (or Turing-computable). This would mean that the intuitive notion of computability is indeed completely covered by these formalisms. This hypothesis is known as “Church’s thesis”. Since the intuitive notion of computability is not formal, there is no formal proof of this hypothesis. We will take a critical look at this hypothesis in a later article.
I am not going to explain any of the mathematical formalizations of computability in any detail. If you are interested, there are books and on-line sources on these topics. For our purposes, it is sufficient to know that several exact formal definitions of the concepts of computability, enumerability and decidability exist.
(The picture is from https://en.wikipedia.org/wiki/File:Alonzo_Church.jpg. It is showing Alonzo Church, one of the fathers of computability theory, alongside people like Kurt Gödel, Alan Turing, Stephen Kleene and some others).