Hacker News Reader

If the correctness of a program requires the ability to terminate, how do these proofs get around the Halting Problem?

You can't, for the general case, prove whether or not a program terminates. For many programs, you can.

These are not machine proofs, so they are not getting round the halting problem.