Does it make sense to use proof to validate that a given monad implementation obeys its laws?
daryoush 2008/9/14 Greg Meredith <[EMAIL PROTECTED]>: > 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" <[EMAIL PROTECTED]> > Subject: Re: [Haskell-cafe] Haskell Weekly News: Issue 85 - September > 13, 2008 > To: "Don Stewart" <[EMAIL PROTECTED]> > Cc: Haskell Cafe <haskell-cafe@haskell.org> > Message-ID: > <[EMAIL PROTECTED] >> > Content-Type: text/plain; charset="iso-8859-1" > > What I am trying to figure out is that say on the code for the IRC bot that > is show here > > http://www.haskell.org/haskellwiki/Roll_your_own_IRC_bot/Source > > What would theorem proofs do for me? > > Daryoush > -- > L.G. Meredith > Managing Partner > Biosimilarity LLC > 806 55th St NE > Seattle, WA 98105 > > +1 206.650.3740 > > http://biosimilarity.blogspot.com > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe