Re: [SC-L] Cost of provably-correct code (was: bumper sticker slogan for secure software)

2006-07-23 Thread der Mouse
>> 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 p

[SC-L] Cost of provably-correct code (was: bumper sticker slogan for secure software)

2006-07-21 Thread David Crocker
Crispin Cowan wrote on 21 July 2006 18:45: >> Yes, you can have provably correct code. Cost is approximately $20,000 per line of code. That is what the "procedures" required for correct code cost. Oh, and they are kind of super-linear, so one program of 200 lines costs more than 2 programs of 100