Comment by impossiblefork

I don't agree that that's exhaustive testing. Full branch test coverage etc., is normal and sensible and it's great, but that's very different from having a proof that given certain preconditions, you will have certain postconditions.