Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!tut.cis.ohio-state.edu!snorkelwacker!bloom-beacon!mcgill-vision!quiche!utility
From: utility@quiche.cs.mcgill.ca (Ronald BODKIN)
Newsgroups: comp.ai
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <2006@quiche.cs.mcgill.ca>
Date: 18 Jan 90 23:05:10 GMT
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <9220@medusa.cs.purdue.edu> <8421@dime.cs.umass.edu>
Reply-To: utility@quiche.cs.mcgill.ca (Ronald BODKIN)
Organization: SOCS, McGill University, Montreal, Canada
Lines: 27

In article <8421@dime.cs.umass.edu> yodaiken@freal.cs.umass.edu (victor yodaiken) writes:
>... 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.
	Unfortunately, untractability theory, ensures us that such a program
will take up to the estimated life-span of the solar system on a computing
device 100 trillion times the speed of a CRAY to solve some problems, otherwise
some problems would be solvable faster than they can be solved (i.e. you can
often show that a computation uses a certain amount of space, so it
will halt within a given amount of time, if at all, so for it to halt
within that length of time is the same as halting -- and if you could
consistently, say, solve NP-hard problems in polynomial time using
this machine, you'd have the result that NP-hard problems are in fact
polynomial etc. etc.)  So, essentially, the "halting problem" is not
nearly so isolated a result.  Indeed, there is NO non-trivial property
of programs that can be solved, and practically it is often totally
untractable to try and do these things using "finite" tricks, just like
the fact that EVERY program can be written using DFA's for as large a set
of input as you like, but its just foolish to try.  It is, of course,
still a fascinating question as to how undecidable "interesting" problems
are, and to what extent things which can not be done in general can be
done in special cases.
		Ron