Kreisel’s No-Counterexample Interpretation: How can we turn proofs in elementary number theory into programs?
For every true number-theoretic statement of the form “For all n there is an m such that P(n, m)” there is a witnessing function f such that for all n, P(n, f(n)) is true. For example, a witnessing function for the statement “For all n there is an m such that m > n and […]
XOR's Hammer 