Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!tut.cis.ohio-state.edu!mailrus!ames!amdahl!pyramid!athertn!joshua
From: joshua@athertn.Atherton.COM (Flame Bait)
Newsgroups: comp.software-eng
Subject: Re: "Correct" IS UNDEFINED!
Message-ID: <17651@joshua.athertn.Atherton.COM>
Date: 1 Feb 90 23:28:17 GMT
References: <7598@hubcap.clemson.edu> <9630012@hpirs.HP.COM> <CLINE.90Jan23165325@cheetah.ece.clarkson.edu> <91033@linus.UUCP> <17142@duke.cs.duke.edu> <17504@joshua.athertn.Atherton.COM> <1306@oravax.UUCP>
Reply-To: joshua@Atherton.COM (Flame Bait)
Organization: Atherton Technology, Sunnyvale, CA
Lines: 51

> = ian@oravax.odyssey.UUCP (Ian Sutherland) writes:
% = joshua@Atherton.COM (Flame Bait) 

% [I talk about seeing many bad definitions of software behavior, and no 
%  good ones.]

>If you're talking about systems like SDI, I agree to a certain extent.
>Most of the attempts I've seen to say what such large systems should do
>are as bad as you say.  

I think the difference is that I think it is impossible to make good
defintions, while you think it is possible, it just has not been done
yet.  Why do you think it is not possible to specify SDI, but it is
possible to specify AT&T's telephone system or a large database application,
or an ADA compiler?  

>I will say that I've seen some reasonably
>generic definitions of both fault tolerance and computer security
>which are both reasonable and sufficiently precise to be input to a
>human or mechanical software verification system.  

Yes, but these are both relatively narrow fields of interest.  You might
be able to prove facts about these limited domains, but I do not believe
that this will translate very well to general systems.  I think there is
a big difference between looking at one aspect of a program as opposed to
looking at the whole thing.  Especially when the aspect is well defined
like security or recovery.

% #ifdef PERSONAL_ATTACK
% If you go back through the "programs can be proven" thread, I think you 
% will find that 80-90% of the people who post in defence of proving
% programs correct post from academic sites.  You will also see that 80-90% 
% of the people who attack this idea post from commercial sites.
% I do not think this is pure chance.  
% #endif

>Was this really necessary Mr. Levy?  Did it serve some important
>purpose?

It was not required for my argument.  That is why I put it at the end of
my posting, with special warning markers.  I added it because I was surprized
at how true it was.  Usually in these discussions there is an even 
distribution of people on each side of the discussion.  I was suprized
at how lopsided this discussion was.

Does it serve some purpose?  I do not know.  It is an interesting fact.
Most people (who have emailed me) have interpreted it as some sort of 
attack on academics, which it was not supposed to be.

Joshua Levy                          joshua@atherton.com  home:(415)968-3718
                        {decwrl|sun|hpda}!athertn!joshua  work:(408)734-9822