Constructive Proofs or Constructive Statements?

Resumen

In this work the following question is considered: is Sergeraert's\Constructive Algebraic Topology" (CAT, in short) really constructive(in the strict logical sense of the word \constructive")? We have not an answer to that question, but we are interested in the following: could have a positive (or negative) answer to the previous question an influence in the problem of proving the correctness of CAT programs (as Kenzo)? Studying this problem, we have observed that, in fact, many CAT programs can be extracted from statements (that is, from the specication of certain objects and constructions), without needing an xtraction from proofs. This remark shows that the logic used in the proofs could be uncoupled with respect to the correctness of programs. Thus, the rst question posed could be unimportant from the practical point of view. These rather speculative ideas will be illustrated by means of some elementary examples, where the Isabelle code extraction tool can be successfully applied.