Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!sharkey!itivax!dhw
From: dhw@itivax.iti.org (David H. West)
Newsgroups: comp.ai
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <4760@itivax.iti.org>
Date: 8 Jan 90 14:55:34 GMT
References: <7578@hubcap.clemson.edu> <25728@cup.portal.com>
Reply-To: dhw@itivax.UUCP (David H. West)
Organization: Industrial Technology Institute
Lines: 17

In article <25728@cup.portal.com> Nagle@cup.portal.com (John - Nagle) writes:
>     I once headed a group of five people that produced a verifier for
>a dialect of Pascal.  It worked, but it was too hard to use to be used
>by most programmers.  It's painfully difficult to convince a mechanical
>theorem prover that your program is correct.  

I think that "most programmers" have never had access to a verifier,
even a "hard to use" one.

Are there any free verifiers out there? (*)

-David West        dhw@iti.org

(*) I expect the number of available free verifiers to be so small
that I don't want to discourage replies by imposing restrictions
concerning language, etc.  I'd be glad if the expectation were
wrong.