Xref: utzoo comp.compilers:758 comp.edu:2928
Path: utzoo!utgpu!jarvis.csri.toronto.edu!cs.utexas.edu!samsung!think!snorkelwacker!spdcc!esegue!compilers-sender
From: mayer@iuvax.cs.indiana.edu (Mayer Goldberg)
Newsgroups: comp.compilers,comp.edu
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <33229@iuvax.cs.indiana.edu>
Date: 17 Jan 90 16:09:15 GMT
References: <7578@hubcap.clemson.edu> <1990Jan16.232703.2368@esegue.segue.boston.ma.us>
Sender: compilers-sender@esegue.segue.boston.ma.us
Reply-To: Mayer Goldberg <mayer@iuvax.cs.indiana.edu>
Organization: Indiana University CSCI, Bloomington
Lines: 11
Approved: compilers@esegue.segue.boston.ma.us

I don't think that the proof theory which produces boring, unintuitive
yet correct code, is meant for you to use to verify your own programs
... I would think it is meant for automatic code generation. This
could be useful, and time saving.

Mayer Goldberg
mayer@iuvax.cs.indiana.edu
-- 
Send compilers articles to compilers@esegue.segue.boston.ma.us
{spdcc | ima | lotus}!esegue.  Meta-mail to compilers-request@esegue.
Please send responses to the author of the message, not the poster.