Subject: RE: [hackers-il] Proving the Correctness of a Proof

From: "Ofir Carny" <[email-masked]>
Date: Wed, 19 Jun 2002 17:13:16 +0200

I will begin by saying I agree to all the comments by Nadav and Tzafrir - I only tried to clarify a
few points and expand others.

There is a whole field of formal algorithmic verification (even though the algorithms
usually only work for a few dozen state variables). 

Moreover, there are also approaches for writing software requirements in a formal 
language, so that they will be verifiable, and then the software will be correct by definition
if it passes verification (although the requirements may not be...), they are not often
used in non critical applications, because they are too hard to read and write.

My point was that for _some_ programs, formal methods cannot prove _some_ correct
statements (e.g. that they always finish). And that if they can then given sufficient time
a program can find and verify that proof.

			Ofir

********************************************************
This email has been scanned by Port Authority.

********************************************************