This work in progress paper presents a methodology for reasoning about the computational complexity of functional programs, which are extracted from proofs. We suggest a first order arithmetic Ta which is a syntactic restriction of Peano arithmetic. We establish that the set of functions which is provably total in Ta, is exactly the set of polynomial time functions. Compared to others feasible arithmetics, Ta is surprisingly simpler. The main feature of Ta concerns the treatment of the quantification. The range of quantifiers is restricted to the set of actual terms which is the set of constructor terms with variables. The second feature concerns a restriction of the inductive formulas.