Path: utzoo!attcan!uunet!aplcen!samsung!think!husc6!m2c!umvlsi!dime!yodaiken
From: yodaiken@freal.cs.umass.edu (victor yodaiken)
Newsgroups: comp.ai
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <8421@dime.cs.umass.edu>
Date: 12 Jan 90 13:41:42 GMT
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <9220@medusa.cs.purdue.edu>
Sender: news@dime.cs.umass.edu
Reply-To: yodaiken@freal.cs.umass.edu (victor yodaiken)
Organization: University of Massachusetts, Amherst
Lines: 12

In article <9220@medusa.cs.purdue.edu> bls@cs.purdue.edu (Brian L. Stuart) 
explains that program verification is impossible because it would violate
the halting problem theorem of Turing. This is true in a very narrow and
uninteresting sense. The problem of program verification is for programs
on actual computing devices, not programs on turing machines. If
someone produced a system which would test to see whether or not a program
could compute its intended result within the estimated life-span of the
Solar system on a computing device 100trillion times the speed of a CRAY,
the system  would , by most accounts be a solution to the program
verification problem. There is nothing in unsolvability theory that
precludes such a system.  Obviously, a far more modest system would
be of great practical use and theoretical interest.