[Haskell-cafe] Haskell Weekly News: Issue 85 - September 13, 2008

Don Stewart dons at galois.com
Sun Sep 14 00:29:20 EDT 2008


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>



More information about the Haskell-Cafe mailing list