Indeed, the halting problem is (amongst other things) just a formal way of saying you can't write a universal theorem prover. Imagine, you could write a program that terminates on the first odd perfect number, or on an unexpected zero of the Riemann zeta function and your "halting problem solver" would give you the answer to questions mathematicians having been breaking their heads over for generations.
It's not clear that the programs we write are anywhere near that kind of complexity. I feel it should be possible to prove some useful properties of programs but we miss some infrastructure for describing the things we want to prove. You can say "all strings must be UTF-8", but how can you explain that to a computer? There's always exceptions to deal with (the result of read() for example).
It's pointed elsewhere in this thread that want you want is to check the program against a model. The problem is, we (often) don't have the model written in a formal way. So we might need a program that tries to determine the model, which we humans then check and which can then be used to check the program. So you can get messages like: function foo is always called with a UTF-8 string, except for that call over there.
Perhaps this can happen during development, so you get prompted: method foo was always called with object bar, and now also with object baz, correct y/n? Depending on the result the model is updated. The question is, can you make this so it doesn't get in your way too much.