I remember my Java IDE in undergrad warned me about an infinite loop, and this was before I learned about the diagonalization proof of the non-computability of the halting problem, one of my favourite proofs ever. The fact that not all programs and inputs can be shown to halt did not stop the engineer who wrote that guardrail for the IDE.

Surely the principia and similar efforts will still yield useful results even if they cannot necessarily prove every true statement from the axioms?

Yes, you can't prove important properties of the class of all programs, but you can prove properties of smaller, limited classes of programs that you are interested in.

So the Java IDE had been able to recognize an infinite loop of the kind you wrote by an algorithm, that can be proven to be correct for a limited class.

On the other hand, you can loop infinitely deciding to exit on the return value of opaque calls to some entity external to your analyzer, and your IDE shouldn't be able to catch that.