[rmcclellan]

Sure, having a virtual human try to solve the problem would be pretty good. However, even the virtual human would never be able to check the specification correctly for every possible program due to the halting problem. In particular, no matter what the specification was, a malicious user could create a program that mimics the virtual human's response and then does the opposite thing (it's the same basic proof that the halting problem is undecidable). By construction then, the virtual human would answer incorrectly when asked whether or not the program matches the specification.

So, academically, even the "virtual human" approach doesn't work since it doesn't answer correctly for every single program. Practically, you're right, having a virtual human would be good enough for most uses.

That said, I wouldn't want to use a virtual human for this due to ethical concerns :-).