> Well typed doesn't even tell you whether a program terminates or not and on what inputs. On the contrary, knowing that a piece of lambda calculus can be simp

> Well typed doesn't even tell you whether a program terminates or not and on what inputs. On the contrary, knowing that a piece of lambda calculus can be simply typed tells me for certain that the program halts for all inputs. If you demand it work for arbitrary programs, then sure, well typed doesn't "even" tell you that. But no procedure can "even" tell you that (including, probably, anything that can be done by our brains), so it's a rather odd choice as a low-bar.