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
On Sat, Sep 13, 2008 at 9:29 PM, Don Stewart
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>