<div dir="ltr">Daryoush,<br><br>One of the subtle points about computation is that -- via Curry-Howard -- well-typed programs are <b><i>already</i></b> 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.<br>
<br>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 <br>
<ul><li>won't leak URLs to unsavory agents</li><li>won't hold on to handles past their garbage-collect-by date</li><li>won't get caught in a 'deadly embrace' (A is waiting for B, B is waiting for A)</li>
</ul>Sometimes, however, and often in mission critical code, you need stronger assurances, like <br><ul><li>this code really does implement a FIFO queue, or</li><li>this code really does implement sliding window protocol, or</li>
<li>this code really does implement two-phase-commit-presumed-abort</li></ul>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. <br>
<br>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.<br>
<br>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. <br>
<br>Best wishes,<br><br>--greg<br><br clear="all">Date: Sat, 13 Sep 2008 22:24:50 -0700<br>
From: "Daryoush Mehrtash" <<a href="mailto:dmehrtash@gmail.com">dmehrtash@gmail.com</a>><br>
Subject: Re: [Haskell-cafe] Haskell Weekly News: Issue 85 - September<br>
13, 2008<br>
To: "Don Stewart" <<a href="mailto:dons@galois.com">dons@galois.com</a>><br>
Cc: Haskell Cafe <<a href="mailto:haskell-cafe@haskell.org">haskell-cafe@haskell.org</a>><br>
Message-ID:<br>
<<a href="mailto:e5b8e9790809132224u3d29b858j5fda8e41b34566eb@mail.gmail.com">e5b8e9790809132224u3d29b858j5fda8e41b34566eb@mail.gmail.com</a><div id=":xq" class="ArwC7c ckChnd">><br>
Content-Type: text/plain; charset="iso-8859-1"<br>
<br>
What I am trying to figure out is that say on the code for the IRC bot that<br>
is show here<br>
<br>
<a href="http://www.haskell.org/haskellwiki/Roll_your_own_IRC_bot/Source" target="_blank">http://www.haskell.org/haskellwiki/Roll_your_own_IRC_bot/Source</a><br>
<br>
What would theorem proofs do for me?<br>
<br>
Daryoush</div><br>-- <br>L.G. Meredith<br>Managing Partner<br>Biosimilarity LLC<br>806 55th St NE<br>Seattle, WA 98105<br><br>+1 206.650.3740<br><br><a href="http://biosimilarity.blogspot.com">http://biosimilarity.blogspot.com</a><br>
</div>