[dhess]

Whoa there. Church-Turing tells us that everything that is computable is computable by a universal Turing machine. It also tells us that a universal Turing machine and the lambda calculus are computationally equivalent. The lambda calculus is untyped. (There are typed lambda calculi, but they are not computationally more powerful than the lambda calculus. Some of them are less so.)

[kenjackson]

Right. Computability says that you can compute any computable function with the lambda calculus. But I'm saying something broader, which is that anything you're trying to model with computation has a type system. IOW, computability theory says that one can model any computable function, while type theory says that one can properly constrain it.

In essence you need both. You can compute if the number five is greater than the color red, but you may want to ensure that you never do.