Secure Coding mailing list archives
Cost of provably-correct code (was: bumper sticker slogan for secure software)
From: mouse at Rodents.Montreal.QC.CA (der Mouse)
Date: Sat, 22 Jul 2006 15:46:18 -0400 (EDT)
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 mouse at rodents.montreal.qc.ca / \ Email! 7D C8 61 52 5D E7 2D 39 4E F1 31 3E E8 B3 27 4B
Current thread:
- bumper sticker slogan for secure software, (continued)
- bumper sticker slogan for secure software Florian Weimer (Jul 20)
- bumper sticker slogan for secure software Pascal Meunier (Jul 20)
- bumper sticker slogan for secure software der Mouse (Jul 20)
- bumper sticker slogan for secure software ljknews (Jul 20)
- bumper sticker slogan for secure software John Wilander (Jul 21)
- bumper sticker slogan for secure software Crispin Cowan (Jul 21)
- Cost of provably-correct code (was: bumper sticker slogan for secure software) David Crocker (Jul 21)
- Cost of provably-correct code (was: bumper sticker slogan for secure software) der Mouse (Jul 22)
- Cost of provably-correct code Crispin Cowan (Jul 23)
- bumper sticker slogan for secure software mikeiscool (Jul 23)
- security half-life and critical mass securecoding2dave at davearonson.com (Jul 21)