This is the sketch and the intuition. As a theory, it does one piece of very convenient work: it explains why we can't solve the Halting Problem in general (we do not possess correct formal systems of infinite size with which to reason about halting), but also explains precisely why we appear to be able to solve it in so many of the cases we "care about" (namely: we are reasoning about programs small enough that our theories are strong enough to decide their halting behavior -- and we discover new formal axioms to describe our environment).

We also appear not to be able to solve the halting problem for many small programs we care about, or at least we haven't been able to solve it yet.
The simplest example is probably the Collatz conjecture, but in general any mathematical conjecture can be reformulated as determining whether some small program that enumerates and checks all candidate proofs halts.