Daryoush,
One of the subtle points about computation is that -- via Curry-Howard --
well-typed programs are *already* proofs. They may not be the proof you were
seeking (there are a lot of programs from Int -> Int), or prove the theorem
you were seeking to prove (Ord a => [a] -> [a] is a lot weaker than 'this
program sorts lists of ordered types'), but they are witnesses of any type
they type-check against. In a system that has principal types, they are
proofs of their principal type. In this sense, the utility of proofs is
widespread: they are programs.
There is a really subtle dance between types that are rich enough to express
the theorems you would have your programs be proofs of and the termination
of type-checking for that type system. That's why people often do proofs by
hand -- because the theorems they need to prove require a greater degree of
expressiveness than is available in the type system supported by the
language in which the programs are expressed. Research has really been
pushing the envelope of what's expressible in types -- from region and
resource analysis to deadlock-freedom. Again, in that setting the program is
a witness of a property like
- won't leak URLs to unsavory agents
- won't hold on to handles past their garbage-collect-by date
- won't get caught in a 'deadly embrace' (A is waiting for B, B is
waiting for A)
Sometimes, however, and often in mission critical code, you need stronger
assurances, like
- this code really does implement a FIFO queue, or
- this code really does implement sliding window protocol, or
- this code really does implement two-phase-commit-presumed-abort
It's harder -- in fact i think it's impossible for bullet item 2 above -- to
squeeze these into terminating type-checks. In those cases, you have to
escape out to a richer relationship between 'theorem' (aka type) and 'proof'
(aka program). Proof assistants, like Coq, or Hol or... can be very helpful
for automating some of the tasks, leaving the inventive bits to the humans.
In my experience, a proof of a theorem about some commercial code is pursued
when the cost of developing the proof is less than some multiple of the cost
of errors in the program in the life-cycle of that program. Intel, and other
hardware vendors, for example, can lose a lot of business when the
implementation of floating point operations is buggy; and, there is a
breaking point where the complexity/difficulty/cost of proving the
implementation correct is sufficiently less than that of business lost that
it is to their advantage to obtain the kind of quality assurance that can be
had from a proof of correctness.
One other place where proofs of correctness will be pursued is in
mathematical proofs, themselves. To the best of my knowledge, nothing
mission-critical is currently riding on the proof of the 4-color theorem.
The proof -- last i checked -- required programmatic checking of many cases.
Proving the program -- that implements the tedious parts of the proof --
correct is pursued because of the culture and standard of mathematical
proof.
Best wishes,
--greg
Date: Sat, 13 Sep 2008 22:24:50 -0700
From: "Daryoush Mehrtash"