Path: utzoo!attcan!uunet!clyde.concordia.ca!jarvis.csri.toronto.edu!cs.utexas.edu!uwm.edu!mrsvr.UUCP!pet16.uucp!hallett
From: hallett@pet16.uucp (Jeff Hallett x5163	)
Newsgroups: comp.ai
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <1862@mrsvr.UUCP>
Date: 12 Jan 90 15:44:20 GMT
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <9220@medusa.cs.purdue.edu>
Sender: news@mrsvr.UUCP
Reply-To: hallett@gemed.ge.com (Jeffrey A. Hallett (414) 548-5163)
Organization: GE Medical Systems, Milwaukee,  WI
Lines: 47

In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.edu (Brian L. Stuart) writes:
>
>His arguments are significant and important practical considerations, but
>there is a more fundamental theoretical issue here.
>
>1)  No program can be verfied to be correct unless it is verified that it
>    produces the correct output.

Proving that  the output correct   is  an insufficient  but  necessary
condition of overall correctness.  Granted that  this is somewhat of a
digression, but one may overlook effects like fault masking  when only
examining output.

>
>The upshot of this is that for any language or programming methodology
>which is verifiable, there will be some programs that can be expressed
>on a Turing Machine which cannot be expressed in this language or
>methodology.  When you ask for verifibility, you ask to sacrifice
>Turing-compatability.  Be careful what you ask for, you may get it.


This is gonna sound stupid, probably, but I'm  not convinced that this
is such a bad thing.   Before you hit that  'F' key, let me  explain a
little.  Turing compatibility is all well and good, but  I think if we
are going to have any major breakthroughs  in computing technology, it
will involve a step beyond Turing machines.  Generally, they still are
too limited to  yield the results we really  need.  I personally  feel
that if we are to make any major advancements in object-oriented or AI
technologies, it  will  involve a major change  in the way  we current
envision  programming  and computing  -   we still  think in  terms of
sequential steps.  OO is slightly  getting  on the right path,  but we
are  still  forced to  reduce  our   great data-driven  systems   into
sequential steps.  Similarly, parallel-processing  is just  a bunch of
sequential steps happening together.

I'm  not  claiming to    be the  great  bearer  of   new and  exciting
breakthroughs here.  I just  toss out  these ideas  as a   dreamer and
speculator on the future.  I don't even have an idea of what the 'new'
stuff must  be - but  I think  we  are  gonna  need  it.  (howzat  for
specific?) 


--
	     Jeffrey A. Hallett, PET Software Engineering
      GE Medical Systems, W641, PO Box 414, Milwaukee, WI  53201
	    (414) 548-5163 : EMAIL -  hallett@gemed.ge.com
"Non Sequitor - Your facts are uncoordinated"; "I am Nomad: I am perfect."