Not necessarily. Isabelle/HOL, an prover not based on CH but on the LCF-architecture, can also do program extraction, see e.g. Program extraction in Isabelle:
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.]
https://wwwbroy.in.tum.de/~berghofe/papers/TYPES2002_slides....