Path: utzoo!attcan!uunet!mcsun!ukc!edcastle!lfcs!arshad
From: arshad@lfcs.ed.ac.uk (Arshad Mahmood)
Newsgroups: comp.ai
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <1596@castle.ed.ac.uk>
Date: 13 Jan 90 13:42:38 GMT
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is> <1990Jan11.015531.20996@world.std.com> <9220@medusa.cs.purdue.edu> <4784@itivax.iti.org>
Reply-To: arshad@lfcs.ed.ac.uk (Arshad Mahmood)
Organization: Laboratory for the Foundations of Computer Science, Edinburgh U
Lines: 50

In article <1990Jan12.030424.1397@world.std.com> bzs@world.std.com (Barry Shein) writes:
>
>The halting problem states (very roughly) "There exists at least one
>program who's halting conditions cannot be determined".
>
>People don't often write that program*, the fact that there was one
>(or a few) theoretically possible counter-example would hardly be
>sufficient to invalidate the concept of automatic program
>verification.

No there are uncountably many of them.

The undecidability of most of these problems is certainly a theoretical
block, which in practice means that if you write a theorem prover
to make sure that all your verifications conditions are satisfied it may
loop forever. It is rarely the case that one would attack such a problem
in such a naive way and usually relies on heuristics (examples
include the very successfull Boyer-Moore heuristics for proving
theorems about inductive LISP programs), which set of heuristics is
most suitable is still undecided (surprise, surprise!) however in recent
years people have developed tools for specifying and reasoning about them
an example of which is Alan Bundy's "Proof Plans", however the area
is still it's infancy.

In practice one would not use theorem provers, and would rely instead
on proof checkers. The latter rely on the user to supply the proof, but
can construct skeleton proofs, maintain libraries, provide tactics
and generally try and make the job simpler. This goes well with our
intuition that proofs provide confidence in our programs rather than any last
say about their absolute correctness (even if one had a measure for it),
proofs can highlight hidden assumptions, contradictory statements in
specifications, etc.

I did not wish to get involved with this discussion since I found those
people who objected to it not even very aware of what was happening
in the field, and to say that it is largely dead is inaccurate, examples
of groups working here in Britain alone are Don Sannella, Mike Fourman, 
Rod Burstall et al here in LFCS,
Bernard Sufrin, Mike Spivey, Joseph Goguen et al in Oxford, PRG, 
Mike Gordon et al in Cambridge, John Darlington, 
Robert Kowalski et al Imperial College,
there are also people in Manchester,Glasgow,London, etc. 

The tools developed so far are naturally somewhat basic, but 'Z' has been
 and continues to be used in industry.

A. Mahmood
Laboraory for the Foundations of Computer Science
Edinburgh University
Scotland