dmehrtash:

>    I have a newbie question....  Does theorem proofs have a use for an
>    application?  Take for example the IRC bot example

>    ([1]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?

Some customers require very high level of assurance that there are no
bugs in the code you ship to them. Theorem proving is one great way to
make those assurances.

-- Don

P.S.

<publicity>

In fact, it's the subject of a talk on Tuesday,

   http://www.galois.com/blog/2008/09/11/theorem-proving-for-verification/

</publicity>