>>2It's neither possible nor necessary to prove correctness of correctness, just like it's neither possible nor necessary to prove logic. Practice is the only proof. Just as the caveman learned the power of logic and science (fire, wheels, etc) by the bumps on his head, just so is the virtue of program verification proven by how rarely formally verified programs exhibit erroneous behavior.