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?