[kenjackson]

Your assumption is the natural order of computation are digital computers. I think some will argue that type systems are inherent in the world. Mass has a type, velocity has a type. mv has a type that is a function of mass and velocity.

Computation is about expressing the type system that is inherent in the computation. Modern computers not having types are an artifact of their implementation, but not of computation per se.

[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.