> 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"

to stop being able to prove "every" thing you only need to 1 counterexample - which Turing found

all explicit examples of unprovable things are very removed from real demand (other than "prove arbitrary program halts", which probably doesn't count as real demand anyway and more of vapordream)