even mathematically impossible to do formally (reducible to the halting problem).

Nah, if the programs are not arbitrary (and I hope they’re not, considering that you chose them) then it doesn’t reduce to that. But you are right that it is not feasible for most industries and he is right that in some industries it is not only feasible but required.