<div dir="ltr">What I am trying to figure out is that say on the code for the IRC bot that is show here<br><br><a href="http://www.haskell.org/haskellwiki/Roll_your_own_IRC_bot/Source">http://www.haskell.org/haskellwiki/Roll_your_own_IRC_bot/Source</a><br>
<br>What would theorem proofs do for me? <br><br>Daryoush<br><br><div class="gmail_quote">On Sat, Sep 13, 2008 at 9:29 PM, Don Stewart <span dir="ltr"><<a href="mailto:dons@galois.com">dons@galois.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">dmehrtash:<br>
<div class="Ih2E3d">> I have a newbie question.... Does theorem proofs have a use for an<br>
> application? Take for example the IRC bot example<br>
</div>> ([1]<a href="http://www.haskell.org/haskellwiki/Roll_your_own_IRC_bot" target="_blank">http://www.haskell.org/haskellwiki/Roll_your_own_IRC_bot</a>) listed<br>
<div class="Ih2E3d">> below. Is there any insight to be gained by theorem proofs (as in COQ)<br>
> into the app?<br>
<br>
</div>Some customers require very high level of assurance that there are no<br>
bugs in the code you ship to them. Theorem proving is one great way to<br>
make those assurances.<br>
<br>
-- Don<br>
<br>
P.S.<br>
<br>
<publicity><br>
<br>
In fact, it's the subject of a talk on Tuesday,<br>
<br>
<a href="http://www.galois.com/blog/2008/09/11/theorem-proving-for-verification/" target="_blank">http://www.galois.com/blog/2008/09/11/theorem-proving-for-verification/</a><br>
<br>
</publicity><br>
<br>
</blockquote></div><br><br>
</div>