I think you have slightly misunderstood the halting problem. There is no computer program H that, for every program P, determines whether P halts. This does not imply that for some particular program Q there is no proof that it halts. In fact in the setting where programs do not take input there is always such a proof (just a trace of the program running to completion). And there are many valid proofs of theorems like "For all x, Q(x) halts" for particular Q. Consider, for example, the case where Q has no control flow at all!

I think it's more that I lean into some of the corollaries that directly factor computation time into account. There is no computer program H that for every program P determines whether P halts faster than running P.

You cannot find/prevent every case of an infinite loop at design time/compile time if the only way to determine a complex enough control flow converges towards halting is to run the full program in a live environment.