How good can a halting detector be?
This isn't a "nice" property, because whether it's true or false depends upon the encoding.

See David et al's Asymptotically almost all $\lambda$-terms are strongly normalizing, which proves what it says in the title. However, this paper also shows that the opposite holds for SKI-combinators (into which lambda-terms can be compositionally embedded). 

In the lambda calculus, a reduction is the equivalent of a step of a Turing machine, and strong normalization is the property that every reduction sequence eventually reaches a normal form -- ie, no further reductions are possible. (Since a given lambda-term may have many valid reductions, strong normalization is a bit like saying a given nondeterministic Turing machine always halts.) So the fact that asymptotically almost all $\lambda$-terms are strongly normalizing means that with probability approaching 1, reducing a large lambda terms will always reach a normal form. 

However, lambda-terms can be translated in a meaning-preserving way into a combinatory calculus such as the SKI combinators (and vice-versa), and in combinator calculi asymptotically all terms loop.