[piano]

> Sure, you can’t in the general abstract case, but my exact point is that you can do this in practice, for programs which we actually write.

No, it can't be done with testing even for practical everyday programs, precisely because you never know how much your program is crossing into the "abstract general case" and which parts of it are more general than you think. Very often the cause of bugs is precisely this - that some part of a program behaves in a more general / less restricted way than the programmer thought.

It can be done with formal verification, but that's a whole another story.