What is the current state of the art in solving the halting problem?
The question as asked is indeed very broad. I give a brief answer here: What are some comparative studies on program termination verification tools?, but that really barely scratches the surface.

I do have several remarks:


In general, once must distinguish between whole program analyses, which are powerful, but do not scale very well for realistic development, and modular analyses which are weaker, but have hope of being integrated in a development environment. Isabelle and Idris both take this approach. As a side note, I'm not sure if this Fuhs et al paper corresponds to the "out of the box" termination check for Isabelle, but it might be enlightening in terms of what the state of the art is.
Termination of higher-order typed programs is difficult, because it involves subtle interactions between the type system features, the inductive types involved, and the "guard condition" required for function definitions. The more complicated the termination check, the less trustworthy the system, since consistency depends on it! These slides by Barras go into some of the nasty details for the Coq system.
Termination for higher-order systems with side effects (references) is particularly nasty. In particular, types are not enough anymore, even in the absence of recursion, see e.g. Landin's knot.