Path: utzoo!attcan!uunet!munnari.oz.au!bruce!cjs
From: cjs@bruce.OZ (Chris Stuart)
Newsgroups: comp.theory
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <1788@bruce.OZ>
Date: 14 Jan 90 07:08:28 GMT
References: <1891@uwm.edu>
Organization: Monash Uni. Computer Science, Australia
Lines: 24

In this discussion, it has been said that certain programs might resist
proofs of correctness, because you can't solve the halting problem and
thus there are programs for which you can't prove termination.

However, the existence or difficulty of a proof of program "correctness"
depends not only on the program, but also the definition of correctness.

Consider a simple program that searches for positive integer solutions to
	x^n + y^n = z^n
where x, y, z and n are all less that 2^20. (This may require handling
integers which take up to 2.5M of storage each!).

I can't prove whether or not this program will print out any solutions.
(I am not a good enough mathematician to tackle Fermat's Last Theorem
directly, and I don't have time to run the program to completion.)

However, I can easily prove that the program will print out all
solutions which do exist within the given range.

For *any* program, there is always *something* that can be proven about
it, even if you can't prove whether or not it terminates. In fact, there
is nearly always something useful which can be proven.

Cheers -- Christopher Stuart