TFA seems to be big on mathematical proof of correctness, but how do you ever know you're proving the right thing?