There is the intuitive idea of an effectively computable function (of one or more natural numbers given as arguments): given the arguments, you can compute the value of the function using a "procedure" (or a set of rules) that does not require any creativity. Example: Addition of two natural numbers n and m. We know how to calculate n+m :-)
How can we formalize this notion of effective computability? On possible formalization is the notion of a Turing computable function, that means a function that can be computed by a Turing machine. One can show that addition, multiplication and many other functions can be computed by a Turing machine.
Now it is clear that every Turing computable function is effectively computable (just use pen and paper and write down what the Turing machine is doing).
The other direction is known as Church's Thesis (named after Alonzo Church) or Church-Turing-Thesis: every effectively computable function is Turing computable.
The thesis can not be proved, since "effectively computable" is an intuitive notion.
Two other formalizations of the notion of effectively computable are abacus computability (similar to Turing machines) and recursive functions. One can show that all these notions are equivalent.
Does anybody know what this principle is called?