It is well known that mathematical proofs often contain (abstract) algorithms, but although these algorithms can be understood by a human, it still takes a lot of time and effort to implement these algorithms on a computer; moreover, one runs the risk of making mistakes in the process.
From a fully formalized constructive proof one can automatically obtain a computer implementation of such an algorithm together with a proof that the program is correct. As an example we consider the fundamental theorem of algebra which states that every non-constant polynomial has a root. This theorem has been fully formalized in the Coq proof assistant. Unfortunately, when we first tried to extract a program, the computer ran out of resources. We will discuss how we used logical techniques to make it possible to extract a feasible program. This example is used as a motivation for a broader perspective on how the formalization of mathematics should be done with program extraction in mind.
|Title of host publication||Theorem Proving in Higher Order Logics (Proceedings 16th International Conference, TPHOLs 2003, Rome, Italy, September 8-12, 2003)|
|Editors||D.A. Basin, B. Wolff|
|Place of Publication||Berlin|
|Publication status||Published - 2003|
|Name||Lecture Notes in Computer Science|