Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!yale!cs.yale.edu!blenko-tom
From: blenko-tom@CS.YALE.EDU (Tom Blenko)
Newsgroups: comp.ai
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <11810@cs.yale.edu>
Date: 17 Jan 90 06:13:55 GMT
References: <16479@joshua.athertn.Atherton.COM> <1455@krafla.rhi.hi.is> <16665@joshua.athertn.Atherton.COM> <10289@microsoft.UUCP> <1928@uwm.edu>
Sender: news@cs.yale.edu
Reply-To: blenko-tom@CS.YALE.EDU (Tom Blenko)
Organization: Yale University Computer Science Dept, New Haven CT  06520-2158
Lines: 30

In article <1928@uwm.edu> markh@csd4.csd.uwm.edu (Mark William Hopkins) writes:
|In article <10289@microsoft.UUCP> jimad@microsoft.UUCP (JAMES ADCOCK) writes:
|>Given that real-world commercial software products of typical size have
|>thousands, if not tens-of-thousands of bugs discovered before shipping,...
|
|You seem so overly predisposed to the prejudice of "programming as engineering"
|as to unnecessarily exclude a concept that is already proven to work.

I am among the skeptical regarding Hopkins' claims. If he has what he
says, this represents a dramatic improvement in the state of software
engineering. And someone who has access to the technology can put
Microsoft, for example, out of business rather quickly.

I would like answers to two questions, at least one of which Hopkins
didn't reply to previously:

	What do you do about memory aliasing? This is, according to any
	treatment I have encountered, a problem whose complexity
	increases at least exponentially with the size of the program,
	and for a C program it would almost certainly require global
	analysis of the program.

	How do you ensure that the specification is any good? I have
	worked with specifications in industry, and I'm sure I've never
	seen one that was complete. I probably have never seen one that
	is both non-trivial and consistent. So where do you get good
	(consistent and reasonably complete) specifications?


	Tom