Are untyped and simply typed lambda calculus mutually exclusive? 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?
 A: 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.
A: That is correct. The simply typed lambda calculus cannot code every algorithm, since every "program" written in it halts.
A: I'm not an expert, but I think I disagree with Philip Wadler's conclusion. We could have a system with two kinds of terms, "total" and "partial". If you're willing to work with partial terms, then you get loops, recursion etc. The total terms wouldn't have this property, but nonetheless there could be a way to go between them. A partial term of type $T$ could feasibly be turned into a total term of type $\mathrm{Maybe} \;T$. And of course, every total term of type $T$ can also be turned into a partial term of type $T$. So the two systems would be interlinked, thereby potentially offering facilities for both logic and computation in one type system.
