🚀 go-pugleaf

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