> Which means that they just luckily don't have to prove anything about any software that might halt...? Or?

the only thing halting problem says is that you can't prove *everything*

feel the difference between "any" and "every"