> 1. The halting problem applies specifically to deterministic systems; there may be a non-deterministic equivalent, but not enough people cared before AI got good.

Making your Turing machine non-deterministic doesn't add any power to it in the sense that the halting problem cares about.

> 2. For practical purposes, it's fine to reject things that take too much effort to prove correct.

Even more so: in practice you write software and proof together. Forget about being able to prove anything about arbitrary software that was written with no proof in mind.

> 3. "Proven correct" is different from "proven to halt eventually". I guess Gödel's incompleteness theorems would be a partial fit, but even then the goal here is to reject anything you can't prove, rather than the much harder (impossible) challenge of proving the validity of all possible statements it might come up with.

Proven correct is a much stronger statement than proven to halt eventually. The form usually has to include the latter.

But yes, as said before, we only prove software that's specifically co-written to be easy to prove.