[amavect]

A few formalizations exist: bounded arithmetic, internal set theory, Nelson's predicative arithmetic.

From Buss's thesis "Bounded Arithmetic": "However, a recursive function may be computable only in a theoretical sense: the time required to compute it may be far larger than the lifespan of the universe. We are more interested in feasibly computable functions, which can be calculated by today's (or tomorrow's) computers."

And then he goes and defines an arithmetic hierarchy for polynomial functions.