In "Proposition as Types" by Philip Wadler we can read that:
The two applications of lambda calculus, to represent computation and to represent logic, are in a sense mutually exclusive.
If a notion of computation is powerful enough to represent any effectively calculable procedure, then that notion is not powerful enough to solve its own Halting Problem: there is no effectively calculable procedure to determine whether a given effectively calculable procedure terminates.
However, the consistency of Church’s logic based on simply-typed lambda calculus depends on every term having a normal form
In my current interpretation, Wadler is essentially saying that untyped lambda calculus is powerful enough to represent any effectively calculable procedure but can't solve its own "Halting problem" (i.e handle self-application). Whereas simply typed lambda calculus can solve it trivially because every term has a form where $\beta$-reduction is not possible (normal form).
I am surprised by the strong wording of Wadler, calling those two "mutually exclusive". Does that mean that simply typed lambda calculus cannot represent any effectively calculable procedure or am I missing the point?
It is deeper than just a property of the simply typed lambda calculus in particular.
There are plenty of ways to extend the simply types lambda-calculus into something that is useful for computations, without letting go op the types. So it's not just a question of typed versus untyped.
Rather, the point is that as soon as you have a general way to write an infinite loop for your computation, "general" meaning that it works no matter which type of value the loop was supposed to have produced if it ever completed, then because of that very fact every type is inhabited and as a result the corresponding logic is inconsistent.
So there can't ever be any calculus that is both useful for expressing arbitrary computations in a natural way, and creates a consistent logic through the propositions-as-types principle.
In light of this fundamental incompatibility, it's remarkable how useful and fruitful as a source of ideas for as well logic and programming the correspondence nevertheless is.