Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!swrinde!zaphod.mps.ohio-state.edu!usc!apple!sun-barr!decwrl!shelby!unix!hplabs!hpda!hpcuhc!runyan
From: runyan@hpcuhc.HP.COM (Mark Runyan)
Newsgroups: comp.software-eng
Subject: Re: Re: "Program Proving"
Message-ID: <2480007@hpcuhc.HP.COM>
Date: 18 Mar 90 23:17:50 GMT
References: <52044@microsoft.UUCP>
Organization: HP GSY/USO/UKL Cupertino, CA, USA
Lines: 18

>/ sean@castle.ed.ac.uk (S Matthews) /  2:46 am  Mar 16, 1990 /
>Anyone who expects to be able to do this after Jones (who, if anybody,
>knows what he is talking about in formal verification) has admitted that
>it is not practical, should expect to be doubted in other statements.
>
>Formal verification is not a snake oil panacea, but some people make it
>sound like one and it is no wonder that reasonable people are sceptical
>of their claims.

Your telling me that formal proofs are *only* useful on new development?
Considering how much old code is out there, I find this slightly 
frightening.

Still, anything that can be used to improve new code is a plus.  But at
the moment, I'm trying to fight fires in old code where total replacement
is *not* considered an alternative.

Mark Runyan