The idea is that the Curry-Howard isomorphism allows you to "play" with constructive mathematics easily. For example, consider the fact that the composition of two functions f and g is continuous if each function is continuous. Suppose f : X -> Y and g : Y -> Z. Then, in pseudo-Haskell syntax, we could say

  continuousf  : Open set in Y -> Open set in X
  continuousg  : Open set in Z -> Open set in Y
  continuousgf : Open set in Z -> Open set in X
  continuousgf = continuousf . continuousg

The idea is that the fact that f is continuous means that we can produce open sets in X given open sets in Y. Now, consider the fundamental theorem of algebra over complex numbers. This says that any polynomial with complex coefficients with degree greater than 0 has at least one complex root. We'd like to have a function

  fta : Polynomial P of degree >0 over C -> (Point x in C, proof that P(x)=0)

which would compute this root. But the thing is, the standard proof (e.g., by Louiville's Theorem) of the FTA is not constructive. The proof is by contradiction: Suppose there were no root. Then we violate some principle of complex analysis that we know is true (Louiville's Thm, or Maximum Modulus Principle, for example). Thus there must be a root.

But this doesn't tell us at all how to compute the root! So instead we need a constructive proof of the FTA in order to produce a root.

So, the idea is that you can't "play" with non-constructive mathematics in programming as you can with constructive mathematics. Our standard FTA proof would look like

  fta : Polynomial P of degree >0 over C -> Exists x. P(x)=0.

But the type of the object that this function produces isn't very fun to play with. We have no idea what the root is!