During the last two decades a systematic program of "proof mining" has emerged as a new applied form of proof theory and has successfully been used in a number of areas of core mathematics. Here one interprets given, prima facie noneffective, proofs in terms of suitable functional programs which exhibit the hidden computational content of the proof. The main tools used are novel forms and extensions of Kurt Goedel's famous functional ("Dialectica") interpretation. We will discuss some specific applications in the context of nonlinear analysis (convex optimization, ergodic theory, game theory and abstract Cauchy problems) resulting in new explicit rates of convergence for iterative algorithms among other things.
