Path: utzoo!utgpu!news-server.csri.toronto.edu!mailrus!cornell!oravax!ian
From: ian@oravax.UUCP (Ian Sutherland)
Newsgroups: comp.software-eng
Subject: Re: Re: "Program Proving"
Message-ID: <1431@oravax.UUCP>
Date: 16 Mar 90 23:05:10 GMT
References: <52044@microsoft.UUCP> <2480006@hpcuhc.HP.COM> <1423@oravax.UUCP> <2870@castle.ed.ac.uk>
Reply-To: ian@oravax.odyssey.UUCP (Ian Sutherland)
Organization: Odyssey Research Associates, Ithaca, New York
Lines: 22

In article <2870@castle.ed.ac.uk> sean@castle.ed.ac.uk (S Matthews) writes:
>Ian should know a *lot* better than this, and severely damages his own
>credibility by saying it. 

I don't know what you think I was saying.  The question is "what is
nontrivial?"  I'm willing to have people post programs, look at them,
and if I think it's reasonable to try to get them through our system
(Ariel), possibly with some modifications, I'll try it.  If I have
some success, I'll report it.  I don't guarantee that I'll even try a
single one of the suggestions posted.  What about this damages my
credibility?

>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.

What is it that I'm expecting to be able to do?
-- 
------
Ian Sutherland		ian%oravax.uucp@cu-arpa.cs.cornell.edu

Sans Peur