What is the difference between proofs and programs (or between propositions and types)? Given that the Curry-Howard Correspondence is so widely spread/extended, is there any difference between proofs and programs (or between propositions and types)? Can we really identify them?
The programming languages people use day to day don't fit so well into the Curry-Howard correspondence, because their type systems are too weak. To say something interesting using Curry-Howard for imperative programs, one needs to have a more sophisticated type system. The book Adapting Proofs-as-programs pushes this angle with the aim of synthesising imperative programs. With dependent types becoming more and more popular, certainly in research functional languages (Agda, Epigram), the distinction is becoming blurrier. Of course you can do program synthesis/extraction within the Coq theorem prover (and presumably others), which is of course based on Curry-Howard.

The Curry-Howard correspondence can also be used in situations where the proofs do not so clearly correspond to programs (or they are not programs anyone will ever run). One example of this is in Proof-carrying authorization. The propositions correspond to statements about who is authorized to do what. Proofs provide the required evidence that a proposition holds, thus an authorization request is permitted. In order to encode the proofs, proof terms are introduced (via Curry-Howard). Proof terms are sent between parties as representations of proofs of the validity of authorization requests, but they are not considered programs.