Curry Howard correspondence and Church-Turing thesis
I'm not sure where you see the dissonance. 

The Church-Turing thesis is a hypothesis stating that Turing Machines (equiv. Lambda Calculus or Recursive Functions) can do anything that we'd think of as computable.

The Curry-Howard correspondence is a much stronger statement that certain types of intuitionistic logic are structurally identical to things kind of like the Lambda Calculus. It doesn't really say which logic it corresponds to, it just shows that you can map the logical constructions in a canonical way to a (typed) computational model and vice versa. If you take different logics, you get different models and vice versa. The models may or may not be Turing-complete, although if we believe the Church-Turing thesis (it does seem to be doing alright so far), if you get a model that's more powerful than a Turing Machine, then you've got something incomputable in there.

Nonetheless, the logic you deal with does limit what you can compute in the corresponding model. For example, the Calculus of Inductive Constructions, which is a type theory and the basis for Coq, only allows types that it can verify have decreasing definitions (i.e. a recursive destruction of the type will terminate), but there are perfectly computable types which it can't verify, so you're locked out of using them.