What is Math Really About? part 3- computation

Whether we are looking at the theory describing a simple phenomenon, or trying to found all of mathematics, we will want to know some things about our ability to investigate the formal theory we have chosen to study. It is natural to ask what things can be proven and dis-proven (questions of computability), and if something can be proven, how long a proof will its proof take (a question of computational complexity). This is the sort of question that began computer science as a distinguishable subject in mathematics, and all systems of computation (Turing machines, grammars, the lambda calculus and its type theories, mu-recursion, etc) can be described as rewriting systems exactly because what they are intended to describe is rewriting in math. It is not possible to prove that these systems describe all things that can be computed because they are the definition of computation (in other words, that is not something to which the notion of proof applies), but in practice the systems mentioned above are accepted for two reasons: a huge number of other systems have been shown to be weaker, or at most as strong, as these systems, and stronger ones (systems of super-Turing computability) don't seem to capture the notion of computation at all.

In some sense computer science is the constructive part of math- that part concerned only with objects that can actually be constructed where truth comes from an explicit proof. This is in contrast with classical math where something can can be "true" in some ultimate sense without being able to give a proof (for example, its possible to prove the existence of an object with some property without being able to describe any particular object with that property). This bring math down to earth- we can't talk about things too large to do computations on, we can't talk about objects that we can't construct.