Look at the Dafny language from MSR: http://research.microsoft.com/en-us/projects/dafny/ http://research.microsoft.com/en-us/projects/dafny/ Your problem is, I

Look at the Dafny language from MSR: http://research.microsoft.com/en-us/projects/dafny/ http://research.microsoft.com/en-us/projects/dafny/ Your problem is, I think, assuming programs have correctness as an intrinsic property. This is not so. Programs can only be correct with respect to something - some idea born in a human mind, transcribed into something the checker understands (here, pre- and post-conditions). If the human mind wants 2+2 to equal 5 in their program, all power to them - they must only ensure this does not cause inconsistency.