[j2kun]

I think this is unfair: you're comparing a trivial observation to a nontrivial theorem, and complaining why the complicated thing isn't as easy to play with as the trivial thing.

The Curry-Howard isomorphism really doesn't add anything to the conversation that wasn't already there. Mathematicians already know what it means for a proof to be constructive or not constructive, and they know it's easier to work with constructive proofs.

Besides, we already know that there is no general way to compute roots of arbitrary polynomials using elementary arithmetic. What you really want is a procedure to find a description of such an x (to arbitrary accuracy, disregarding efficiency), and these are a dime a dozen.

[wolfgke]

> Mathematicians already know what it means for a proof to be constructive or not constructive, and they know it's easier to work with constructive proofs.

It is often more easy to prove that some object exists (by contradiction) than to construct such an object.

For example: by applying Zorn's lemma it is easy to prove that any vector space has a Hamel basis. But it is often non-trivial to construct such a basis.