As good as you can get without being able the read the programmer's brain to figure out what they really wanted in the first place. To talk about correctness formally in the first place, you need to specify what you want and when you do that there is no guarantee that that is actually what you want.