> There’s probably a practical argument to be made against the theoretical possibility of building such a system: I think that just the halting problem is proof that we cannot implement a system that does this.

I think the halting problem only tells you that you cannot, in general, opinionate on what the program does, without expending an amount of computational effort equivalent to running that program. A better counterpoint is that you can't know ahead of time what values will be returned by IO calls.

But then, none of that really matters, because aiming for perfection is the wrong approach. You can make a tool described by the article, if you accept that it'll need to be advised sometimes. That is, at any point where the tool can't compute something - a value of a variable taken from the network, a function to call through a pointer indirection, etc. - it can ask you to give it a default value, give it additional assumption.

You'd also bound it using explicit heuristics, so it doesn't e.g. get stuck in long loops. Simulation of a marked bit of code takes more than 10ms? "Sorry, nope, can't process that." Then you could add options to annotate the offending loop, telling the simulator to finish it after at most 20 iterations. Or something like this. This tool would be a dialogue with code, not a batch job.

We know it's doable, because all such tool would do is to automate the thing we do when looking at code - running pieces of it in our head. In a way, it's just a different interface for doing the same thing you might be doing with unit tests - except it would be transient, and free to exercise any internal code in your program, not just poke at public module interfaces.