Here's my problem : I know from Curry-Howard that simply typed lambda-calculus is isomorphic to natural deduction.
Now I know that natural deduction admits cut-elimination. I also know that the pullback of cut-elimination through Curry-Howard is reduction of terms (aka execution of a program).
So, I should deduce that every term strongly normalizes, but that implies that simply typed lambda-calculus is not Turing-complete (or it would have halting-problem-like limitations), which annoys me. Lambda-calculus is famously Turing-complete, isn't it?
Is the mistake the confusion between typed and untyped lambda-calculus? If so, why do we always say that Curry-Howard is a correspondance between proofs and programs if it only maps proof to very particular programs that always halt?
Thanks for helping me!
Your reasoning is right. Unlike untyped lambda calculus, simply typed lambda calculus is strongly normalizing. And unlike untyped lambda calculus, simply typed lambda calculus is not Turing complete.