Extraction of terms written using Fixpoint isn't really the Curry-Howard correspondence. Instead, the correspondence is between (for example) proofs of correctness and terms in the Calculus of Constructions.

[Fixpoint terms are also CIC programs, so there's a sense in which they're related, but it's not really about Curry-Howard.]