Yet I can give you an estimate of the runtime of multiple programs I use to an accuracy within seconds (order of magnitude is hours). The halting problem itsel

Yet I can give you an estimate of the runtime of multiple programs I use to an accuracy within seconds (order of magnitude is hours). The halting problem itself is a good estimate for computational complexity (i.e. can my thing simulate a TM) and makes statements for the general case, but that's just it: the general case. There are a whole class of programs/languages that are decidable (i.e. they will terminate) and that can be proven as well by automated means. Now this does depend on what you mean with sufficiently complex, but for special programs you can prove a lot of things (by hand); the halting problem does not prevent that. However, a side effect is that you may not be able to prove that property for the program you want.