Xref: utzoo comp.ai:5477 comp.arch:13102 comp.databases:4587 comp.edu:2882 comp.object:715
Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!ames!think!snorkelwacker!spdcc!merk!xylogics!world!bzs
From: bzs@world.std.com (Barry Shein)
Newsgroups: comp.ai,comp.arch,comp.databases,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <1990Jan11.015531.20996@world.std.com>
Date: 11 Jan 90 01:55:31 GMT
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is>
Organization: The World @ Software Tool & Die
Lines: 34
In-Reply-To: snorri@rhi.hi.is's message of 10 Jan 90 14:25:30 GMT


Yes, the flap in the early 80's was over automatic program
verification. It seemed that DOD was considering putting $150M into
this so the debate became quite bloody.

The automatic program verification proponents lost. Perlis gave a good
talk on why, it went something like:

	In order to determine if a program is correct another
	program would have to build some sort of model to
	compare it against. This would be, presumably, from
	some sort of abstract specification of what the program
	is supposed to do.

	If the verifier could build that model it could translate
	the specifications into the program. So why bother to
	write a program to be verified at all? Why not just write
	a high-level specifications compiler (why indeed, no one
	knows how, but verification was being passed off as something
	palpable to work on, like just a big math proof generator.)

There were some corrollary observations, like what exactly would such
a verifier be able to tell us? Presumably either "yes this program is
correct" or "no, this program is not correct". That's of questionable
value. If it could tell us useful detail about why it was correct or
not then, again, we are led to the conclusion that it could write the
program.

Also some amusing concerns about verifying the verifier.
-- 
        -Barry Shein

Software Tool & Die, Purveyors to the Trade         | bzs@world.std.com
1330 Beacon St, Brookline, MA 02146, (617) 739-0202 | {xylogics,uunet}world!bzs