[xgk]

> separate safety from the much more complex liveness

True, and with program logics, you can choose partial correctness vs total vs generalised correctness.

Itt's even worse in practise. With many contemporary dependently typed languages you'll have to worry about termination even during programming, even before thinking about verification.

The Curry-Howard prover advocates seem to regard this as a solved problem ("just distinguish programs from proofs by way of a typing system, problem solved") but has this solution been implemented in any mature systems as of 2017?