On Sat, 13 Sep 2008 21:06:21 -0700, "Daryoush Mehrtash"
I have a newbie question.... Does theorem proofs have a use for an application? Take for example the IRC bot example ( http://www.haskell.org/haskellwiki/Roll_your_own_IRC_bot) listed below. Is there any insight to be gained by theorem proofs (as in COQ) into the app?
Yes. Basically, if you can prove that the program is correct, then you don't need to test it. While proofs can become very tedious for huge programs with many different kinds of control flow involving very complicated logic, if the program size can be shortened to a reasonable size, then proofs can help shorten development time. This was actually part of the motivation for developing Haskell as a pure functional programming language (i.e., one that prohibits side effects -- see http://www.haskell.org/haskellwiki/Functional_programming). It is generally easier to write proofs for pure functional programming languages than for impure ones. Theorem provers help to automate the process of writing proofs for programs. Djinn (see http://lambda-the-ultimate.org/node/1178) is an example of a theorem prover for Haskell. Given a (Haskell function), it returns a function of that type if one exists. Here is a sample Djinn session (courtesy of http://lambda-the-ultimate.org/node/1178):
calvin% djinn Welcome to Djinn version 2005-12-11. Type :h to get help. # Djinn is interactive if not given any arguments. # Let's see if it can find the identity function. Djinn> f ? a->a f :: a -> a f x1 = x1 # Yes, that was easy. Let's try some tuple munging. Djinn> sel ? ((a,b),(c,d)) -> (b,c) sel :: ((a, b), (c, d)) -> (b, c) sel ((_, v5), (v6, _)) = (v5, v6)
# We can ask for the impossible, but then we get what we # deserve. Djinn> cast ? a->b -- cast cannot be realized.
# OK, let's be bold and try some functions that are tricky to write: # return, bind, and callCC in the continuation monad Djinn> type C a = (a -> r) -> r Djinn> returnC ? a -> C a returnC :: a -> C a returnC x1 x2 = x2 x1
Djinn> bindC ? C a -> (a -> C b) -> C b bindC :: C a -> (a -> C b) -> C b bindC x1 x2 x3 = x1 (\ c15 -> x2 c15 (\ c17 -> x3 c17))
Djinn> callCC ? ((a -> C b) -> C a) -> C a callCC :: ((a -> C b) -> C a) -> C a callCC x1 x2 = x1 (\ c15 _ -> x2 c15) (\ c11 -> x2 c11) # Well, poor Djinn has a sweaty brow after deducing the code # for callCC so we had better quit. Djinn> :q Bye.
Other theorem provers include COQ (see http://coq.inria.fr/) and Sparkle (see http://www.cs.ru.nl/Sparkle/) (a theorem prover for the alternative non-strict, purely function programming language Clean (see http://clean.cs.ru.nl/)). -- Benjamin L. Russell