[lug] can't make this stuff up, folks...

[Zan Lynx]

On 10/19/09 5:44 PM, Bear Giles wrote:
> NASA is CMM 5 and as I understand it requires every line to be traced
> back to a specific requirement.  I don't know if it has to be formally
> proven as well.(*)  Medical devices aren't as strict but I'm sure
> they're also pretty strict.  Both have high cost-per-line but the cost
> of failure is enormous.
>
> But DOD? :-)
>
> (*) Provability is an interesting concept and I've used it to find and
> fix a few corner cases.  In one case I overheard subsequent developers
> complaining about the 'bloat' and about a year later high-fiving
> somebody else who found and fixed an obscure bug.  Gosh, I wonder what
> that bug was and how it was introduced. :-)  But my experience has been
> that provability mostly proves how poorly defined the problem is.

Right.

By the time you've proved the code, you have basically rewritten the 
code over again in the proofing language.

This still leaves all the bugs that are caused by the programmer not 
understanding a piece of the problem. This class of bugs is very large.

For example: what good does it do to prove that some program to parse 
email addresses is correct if the programmer and proofer did not realize 
that user+tag-tag at example.com is a valid email address?
-- 
Zan Lynx
zlynx at acm.org

"Knowledge is Power.  Power Corrupts.  Study Hard.  Be Evil."