The Halting problem as a burden for this kind of code analysis is very overstated. What you do is instruct the compiler how to infer timing inductively on a lan

The Halting problem as a burden for this kind of code analysis is very overstated. What you do is instruct the compiler how to infer timing inductively on a language of all basic internal and I/O ops. And of course it's 2018, nothing stops us from saying "Your software needs training." We can go from a somewhat conservative binding that is then informed by runtime metrics to be very precise for a given deployment and as long as we hold the system static for that measurement, it's pretty fair. As for Hardware verification, I agree it's a harder problem in some ways, but since there is no obfuscation of the important timing quantities it also gets easier.