Curry Howard correspondence and Church-Turing thesis

Question

Curry-Howard correspondence states the equivalence between logic/deduction and types/programs.

The Church-Turing thesis states the equivalence of some models of computation. Specifically, all computable functions can be written both on a Turing Machine and in Lambda Calculus.

Not all logics are equivalent however. 2nd order logic can quantify over sets whilst 1st order can't.

Can someone explain the dissonance? Can some computable functions be expressed at a "higher-level" but not at a "simpler-level"?

[CLARIFICATION]

If I define a model for computation off say 2nd order logic whilst the Turing Machine is a model for 1st order logic, then does that mean my hypothetical language can compute "uncomputable" functions? It appears so to me because 2nd order logic is more powerful than 1st order logic. This is clearly nonsense because Haskell is based off a flavor of 2 order logic (system F with extensions) but isn't more powerful than say C: any program achievable in Haskell is achievable in C. The mapping (or equivalence) between logic and computation does not appear to preserve the notion of strength: 2nd order logic is stronger than 1st order logic but programming languages off 2nd and 1st order logic have the same strength. Does that make sense?

The only conclusion I can come to is that the relationship between logic and types is not a straightforward mapping. The Turing Machine is not based off any specific logic and that any logic/deductive system can be mapped to the Turing Machine. Can you confirm?

[CLOSING WORDS]

I think that my mistake is in not realizing that there is a large divide between the colloquial "program" and programs in the context of types.

Haskell which is based on a stronger, more expressive type system does indeed provide stronger, more expressive programs. These programs are stronger in the sense that more can be guaranteed about them (in the same sense as "type safe"). This does not mean that Haskell can "compute" more; it is still merely Turing complete.