>In the general case, we can't of course, as Turing proved.
Not quite. Turing proved that no single algorithm cannot solve the halting problem for all machines; it has always been trivial to show that we can answer the halting question for many machines we care about, often because they are specifically designed to always halt.
Chaitin elaborated this into a detailed theory of quantified incomputability, showing (roughly) that any N-bit axiomatic system could decide the halting problem only for machines composed of strictly less than N bits of information (Kolmogorov complexity).
So the question is either, depending on your philosophy of mathematics, how we locate ontologically special cases where halting proofs are possible, or how we obtain the information we put into our axioms that allows us to write halting proofs for increasingly complex programs.