Has anyone ever written a piece of code that's really so difficult for a human to read and figure out whether it halts? Obviously it's not hard to imagine theoretical examples of a program so large nobody could figure it out within a human lifetime, but I'm not entirely convinced for real programs written by humans that checking for haltability is likely to be harder than checking for following coding standards (unless your coding standards consist purely of such narrowly and explicitly defined rules that it's 100% automatable). Just because a single algorithm that works for all possible programs can't exist doesn't mean that it's necessarily difficult for any (or even most) actual programs humans might write.