Xref: utzoo comp.ai:5526 comp.arch:13162 comp.databases:4623 comp.edu:2906 comp.object:739
Path: utzoo!attcan!uunet!mailrus!cs.utexas.edu!uwm.edu!csd4.csd.uwm.edu!markh
From: markh@csd4.csd.uwm.edu (Mark William Hopkins)
Newsgroups: comp.ai,comp.arch,comp.databases,comp.edu,comp.object
Subject: Program verification is a proven concept
Message-ID: <1888@uwm.edu>
Date: 14 Jan 90 02:21:43 GMT
References: <7578@hubcap.clemson.edu> <25711@cup.portal.com>
Sender: news@uwm.edu
Reply-To: markh@csd4.csd.uwm.edu (Mark William Hopkins)
Followup-To: comp.ai
Organization: University of Wisconsin-Milwaukee
Lines: 19

In article <25711@cup.portal.com> mmm@cup.portal.com (Mark Robert Thorson) writes:
>There was an excellent article about 10 years ago in CACM on this.
>I believe the title was "The Social Process and Proofs of Program
>Correctness".  This article marked the death of program verification;

I must've missed the boat: I always prove my programs correct.  Pathologies
in provability (which are theoretically guaranteed) almost always indicate
flaws in design.  Therefore undecibeability is actually an AID in program
verification, not an obstacle.

Programs in even languages like C, Pascal can be manipulated via a set of
(complete) algebraic rules -- which form a foundation for the semantics
of the language in question.  I use such rules all the time.

>... from that point on the "conventional wisdom" was that program
>verification was a dead-end for research.  In retrospect, it's hard
>hard to see why this wasn't obvious from the very beginning.

Oh, the irony...