Path: utzoo!attcan!uunet!cs.utexas.edu!uwm.edu!csd4.csd.uwm.edu!markh
From: markh@csd4.csd.uwm.edu (Mark William Hopkins)
Newsgroups: comp.ai
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <1891@uwm.edu>
Date: 14 Jan 90 03:28:28 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> <1596@castle.ed.ac.uk>
Sender: news@uwm.edu
Reply-To: markh@csd4.csd.uwm.edu (Mark William Hopkins)
Organization: University of Wisconsin-Milwaukee
Lines: 28

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.

In article <1596@castle.ed.ac.uk> arshad@lfcs.ed.ac.uk (Arshad Mahmood) writes:
>No there are uncountably many of them.

The fact that you are constantly writing programs that are easy to verify
and understand (wherever possible) dictates that you never encounter any of
the pathological cases.  Therefore undecidability is actually an AID in
guiding the design of your program.  It's good software engineering to
write your programs in a straightforward fashion as possible.  So a
verifier (if automated) would actively refuse to consider software beyond
a certain level of complexity and "tell" you to rewrite it so that it
makes sense.

This not only means that verifiability is a proven concept, but that it is
also a crucial tool to good software design.

So, as an empirical fact, there is no humanly achievable process that cannot
be emulated by verifiable software (where verification is done via a
uniform algorithm).