Subject: Proving the Correctness of a Proof

From: Shlomi Fish <[email-masked]>
Date: Tue, 18 Jun 2002 20:24:16 +0300 (IDT)

I am now reading with interest the book "The Mythical Man-Month" by
Fredrick P. Brooks Jr. In it there is a reprint of an article he wrote
by the name of "No Silver Bullet - Essence and Accident". In it he claims
that there would be no silver bullet for eliminating bugs from programs in
the forseeable future.

One of the suggestions he criticizes is proving the correctness of
programs, because they too can have bugs. This made me thinking: is it
possible to write or adjust a program so that it will verify the
correctness of mathemtical (or more specifically algorithmical) proofs? I
don't mean that it would try to prove it itself, but that it would just go
over it and make sure it doesn't makes a false claim or misses something.

With an encompassing enough database of theorems and algortihms, it may be
possible to verify many such proofs with ease.

Regards,

	Shlomi Fish

There is no IGLU cabal! The former cabalists are trying to prove the
correctness of a program that prove the correctness of proofs of other
programs.

----------------------------------------------------------------------
Shlomi Fish        [email-masked]
Home Page:         http://t2.technion.ac.il/~shlomif/
Home E-mail:       [email-masked]

"Let's suppose you have a table with 2^n cups..."
"Wait a second - is n a natural number?"

---

From: "Nadav Har'El" <[email-masked]>
Date: Tue, 18 Jun 2002 21:05:17 +0300

On Tue, Jun 18, 2002, Shlomi Fish wrote about "[hackers-il] Proving the Correctness of a Proof":
>...
>...

Formal Verification of software (or hardware, like VLSI) should not be
compared to a single mathematical proof, but rather to a whole book of
proofs (e.g., think of Russel & Whitehead's Principia Mathematica).

Why? A proof of a single theorem takes a number of axioms, and a theorem
and then purports to be a "legal" series of derivations starting with these
axioms and ending with the theorem. With a formal language (a la Russel
and Whitehead's), the proof can be written in a manner that can be verified
by a computer.

A computer program or algorithm is different, however. You define the
algorithm's code (one of your axioms) and the enviroment in which it
runs (the other axioms) but then you want to prove many theorems. Your
theorems may include the (alleged) facts that the algorithm halts on
all inputs, does it in (say) O(NlogN) time, and does "it's job". The
latter is in itself hard to specify and usually requires making and
proving many theorems. Even in simple concepts/algorithms - e.g., a
"mutex", you'd end up making theorems for the correctness of the
algorithm, like "two threads can never own the mutex at the same time",
"no thread can ever be starved", etc.

So even if you have a perfect proof-checking or proof-finding software
(such formal verification IS available, although it obviously cannot
solve everything, Goedel, you know...), it is still up to you to specify
*what* you want to prove or verify, and in that that specification you might
have bugs. It's not always easy to define what your demands from the software
are. For example, imagine you're the guy who needs to formally verify (i.e.,
prove using a proving tool) the correctness of the software that runs the
traffic lights in some neighborhood. What are your requirements? You want
to prevent collisions (two lights going green in a single intersection at the
same time), and starvation (a single light never becoming green). Are these
requirements enough for a "correctly" functioning traffic-light system? Are
you sure? How are you so sure?

Returning to the book comparison, Russel & Whitehead's book (if anyone
haven't heard of it, it's a book building logic and set theory from
axioms, in a VERY formalistic almost unreadable-for-humans format),
is filled with proofs, all of them absolutely correct. Does it mean
that Russel & Whitehead have succeeded in proving that set theory is
completely correct, consistent and complete? No, unfortunately it doesn't,
as Goedel showed a few years after they published their book, shattering
Russel & Whitehead's dreams and making a mockery of their monumental
work (well, I'm exaggerating, their work is still considered important, but
it's not as important as they intially hoped it would be). Everything they
proved was right, but some things they didn't consider or prove (like set
theory's "completeness") turned out to be possibly false or unknown.

So don't expect to hear the announcement of a general A1 [1] operating system
in the near future ;)

[1] See the NSA's Orange Book. I googled for an online copy, and found one
in http://jcs.mil/htdocs/teinfo/directives/soft/ds5200.281.html and one
in http://www.astrolox.com/libraryc/orange.html

-- 
Nadav Har'El                        |      Tuesday, Jun 18 2002, 9 Tammuz 5762
[email-masked]             |-----------------------------------------
Phone: +972-53-245868, ICQ 13349191 |When everything's coming your way, you're
http://nadav.harel.org.il           |in the wrong lane.