Re: Intervention needed?

[Maciej Sobczak <see.my.homepage@gmail.com>]

> > For some N% of Ada programs, will a computation of a proof be
> > predictably finished in time? .. Static knowledge is a privilege not
> > shared by many, or much, I suppose.
> 
> If you haven't got some reasoning in your head that the program is
> pointer-correct, you shouldn't deploy it.

This is an appealing perspective, but I agree that the privilege is not available in all situations (SPARK allows unchecked portions of code for a reason).

Which brings a potentially interesting question - what if the reasoning in my head has a continuous measure of correctness? Like, say, I'm 95% confident that the reasoning is correct? Should I deploy my system or not? The mechanical proof will fail 100% of the time, but that does not mean that the software is entirely useless for my user, who also has his own continuous measure of risk and level of failure acceptance.

The ability to work with continuous measures is what is practiced in every other engineering discipline (including critical ones!), yet the formal-method priests like you prevent me from deploying my acceptably correct programs. I find it a *limitation* of your methods, not mine.

Could you please fix your methods so that I can deploy my almost-certainly-correct system, like everybody else does, instead of forcing me to use tools that are demonstrably unfit for today's market needs? Thank you.

(disclaimer: playing the devil's advocate for a reason)

-- 
Maciej Sobczak * http://www.inspirel.com