>> Yes, you can have provably correct code.

Perhaps.  But then you have bugs in the prover (and thus proof)
instead.  Human mistakes if it's human proof, bugs in the code for
automated proof.  You also have bugs in the spec that you're proving
the code conforms to (unless you're simply trying to prove something
like "this code never writes outside an array's dimentioned bounds",
which is not what I usually take "provably correct code" to mean).

/~\ The ASCII                           der Mouse
\ / Ribbon Campaign
 X  Against HTML               [EMAIL PROTECTED]
/ \ Email!           7D C8 61 52 5D E7 2D 39  4E F1 31 3E E8 B3 27 4B
Secure Coding mailing list (SC-L)
List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l
List charter available at - http://www.securecoding.org/list/charter.php

Reply via email to