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

From: "Ofir Carny" <[email-masked]>
Date: Wed, 19 Jun 2002 14:35:31 +0200

IIRC:
Proving that a formal proof is correct is relativly easy (P). 
Finding said proof is an NP-complete time trivial (code complexity-wise) expansion.

About Russel & Whitehead's book: IIRC they did consider the completeness question, and until Godel, it
was expected that a proof for completeness would soon follow. 

What godel proved was that no formal proof system can be complete.

The part about if a program stops for all inputs, in know as the halting problem and shown to be unsolvable
by turing: http://www.cs.washington.edu/homes/csk/halt.html (the beyond the scope part is church's theorem),
but the proof is similar.

		Ofir

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

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

---

From: "Nadav Har'El" <[email-masked]>
Date: Wed, 19 Jun 2002 15:34:36 +0300

> Finding said proof is an NP-complete time trivial (code complexity-wise) expansion.

This is true, but Formal Verification software still exists. The idea is
usually [1] that you have a relatively-simple formal specification of your
system, and the software builds graphs (very large ones, usually), or BDDs,
of states from this specification. Then you make claims that the software
tries to "prove" - these claims are translated to graph-theoretic claims
(like: the graph has a cycle, there is no cycle starting in node N, such-
and-such node is reachable, etc.) and graph algorithms (which are in P,
hopefully) are used to make these "proofs" (or when the claim is wrong,
find a counter-example which comes in very handy when debugging the system).
It obviously cannot verify every system and every type of claim, but I've
seen it work for real applications in telephony, VLSI design, and so on.

[1] Correct me if I'm wrong, because it's been 9 years since I last had
anything to do with formal verification; I also never formally studied the
subject - I only briefly worked in a group that worked on it. If anyone
here studied this subject or knows it well, please feel free to correct
the rubbish I'm writing here.

Anyway, even NP algorithms are fine if N is small (let's face it, you
can't verify a 10-million-line code like Open Office...).

But in any case, my point was different: that even if you do have a working
and fast-enough proving/verification system, your program might still contain
"bugs" because you didn't actually formally-verify everything that you should
have.
Just ask a teacher in a graph-theory course if he never saw errors like this -
people handing in an incorrect algorithm, which has a "proof" that seems
correct, but its problem is that it doesn't really prove all the necessary
requirements of the algorithm ot in all cases.

> but the proof is similar.

Again, it can be solved in specific cases with acceptable resources.
For example, consider the traffic-light algorithm example: can it suddenly
"hang" forever (i.e., enter a cycle of states) and stop showing any of the
lights? It's quite possible to prove (e.g., by looking at the state graph
and showing it does not contain cycles that do not have a timer on the edges)
that it doesn't, given the appropriate specification for the algorithm.

-- 
Nadav Har'El                        |    Wednesday, Jun 19 2002, 9 Tammuz 5762
[email-masked]             |-----------------------------------------
Phone: +972-53-245868, ICQ 13349191 |Snowflakes are very fragile, but look
http://nadav.harel.org.il           |what they can do when they stick together!

---

From: Tzafrir Cohen <[email-masked]>
Date: Wed, 19 Jun 2002 16:15:54 +0300 (IDT)

> complexity-wise) expansion.

But what exactly is the proof system?

What exactly is the theorem you want to prove?

How do you state that "mozilla is bugfree"?

(let alone the fact that there are some contradicting evidences. e.g. in
buzilla.mozilla.org)

Even if you manage to formalize such a proof system?

What will be the size of the theorem that you'll have to prove?

And are you really sure that this is the correct proof? that you haven't
made a small typo? [can you prove it? :-p]

You see, the problematic step is how to formalize the RealLife situations
and requirements. This goes even beyond the theoretical limitations
imposed by modern CS.

-- 
Tzafrir Cohen
mailto:[email-masked]
http://www.technion.ac.il/~tzafrir