It's only impossible to write a program that can be feed with any completely arbitrary program and input and yet determine all the time if it will halt or not.
What few people realize, is that most completely arbitrary programs are very uninteresting. More interesting programs have characteristics that would very often allow to statically prove that all of their loops that should terminate indeed will terminate. And even interesting loops for which it would not be in the first time possible to determine that often gain in clarity from being slightly changed so that the tool can do its work.
IIRC MS has a tool that does sort of that for windows drivers.
What few people realize, is that most completely arbitrary programs are very uninteresting. More interesting programs have characteristics that would very often allow to statically prove that all of their loops that should terminate indeed will terminate. And even interesting loops for which it would not be in the first time possible to determine that often gain in clarity from being slightly changed so that the tool can do its work.
IIRC MS has a tool that does sort of that for windows drivers.