It is well known that restricting induction to existential formulas yields primitive recursive arithmetic. The computational nature of theorems falls out here transparently from the structure of their proofs, without obstructing the theorem prover, human or automated. This talk surveys similarly transparent properties of proofs, in both first and higher order formalisms, which guarantee that the theorems proved are in feasible fragments of mathematics, such as poly-time and poly-space.