[AnimalMuppet]

> So, Peano arithmetic is just too loose and fuzzy for my taste. It's full of things which aren't numbers...

OK.

> In type theory every definable natural number is a program which evaluates to a concrete finite numeral.

To me, that sounds like type theory is also full of things that are not numbers, namely computations. ("Evaluates to a natural number" != "is a number".)

[Kutta]

Evaluation is always implicitly used in any sort of mathematical formalism. "2 + 2" is a program which evaluates to "4". Type theory just makes the computation arising from substituting definitions rigorous. Not letting "2 + 2" be equal to "4" by definition would be weird and inconvenient.

[AnimalMuppet]

I get that evaluation is always implicit (or at least implicitly assumed to happen). My quarrel is with "evaluation == program == computation", and even more with the reverse: "a number == computation that would produce the number, therefore number == computation".