 Every constructive proof embodies an algorithm that, in principle, can be extracted and recast as a computer program; moreover, the constructive proof is itself a verification that the algorithm is correct — that is, meets its specification. One major advantage of Martin-Löf’s formal approach to constructive mathematics is that it greatly facilitates the extraction of programs from proofs. This has led to serious work on the implementation of constructive mathematics in various locations (see Martin-Löf [1980], Constable [1986], Hayashi &amp; Nakano [1988], Schwichtenberg [2009]). Some recent implementations of type theory for proof extraction are Coq and Agda (see the links in Other Internet Resources).