14 Sep
2008
14 Sep
'08
12:29 a.m.
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>