[mrkeen]

The argument is that 'the program returns' is strictly easier to prove than 'the program returns the correct answer'. If the first is impossible, then the second is too.

I'm all in favour of sidestepping the argument by having our languages more resemble System F or some polymorphic lambda calculus.

[WorldMaker]

Though still useful to remember that some of the earliest mathematical write ups of the Halting Problem were also by Alonso Church and directly in the lambda calculus. The Church-Turing Theorem is a lasting reminder that the two worlds imperative and functional describe the same algorithms (form the set of Turing Completeness).

[mrkeen]

It depends on the type system you choose to apply to LC. Simply-typed LC terminates.

You have to include a construct that introduces general recursion to make it Turing complete.

There's a cool practical space within those constraints that needs more exploration.

Non-total functions can call total functions, but not vice-versa.

Imagine a web server whose main loop is non-total, because you want it to stay up. But each route is total, to guarantee termination.