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>

On 2008 Sep 14, at 1:24, Daryoush Mehrtash wrote:

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?

Assurance of correct operation; for example, a mathematically provable lack of security holes, assuming you can describe its proper operation in terms of suitable theorems (which, for a simple bot like that, is not so difficult). -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH

On Sun, Sep 14, 2008 at 5:56 AM, Thomas M. DuBuisson wrote:

...

What would theorem proofs do for me? Imagine if you used SmallCheck to exhastively test the ENTIRE problem space for a given property. Now imagine you used your brain to show the programs correctness before the heat death of the universe...

Proofs are not features, nor are they code. What you prove is entirely up to you and might not be what you think. Take, for example, the issue of proving a sort function works correctly [1].

I'm not saying this to discourage complete proofs, but just cautioning you that proving something as unimportant and IO laden as an IRC bot probably isn't the best example. Do see the linked PDF, and [2] as well.

Oh, and for examples where people should have used FM, search for 'ariane 1996' or the gulf war patriot missle failure

TomMD

[1] http://www.cl.cam.ac.uk/~mjcg/Teaching/SpecVer1/Lectures/pslides07x4.pdf [2] http://users.lava.net/~newsham/formal/reverse/

One thing have always bugged me: how do you prove that you have correctly proven something? I mean, when I write a code I'm formaly stating what I want to happen and bugs happen. If I try to prove some part of the code I write more formal text (which generally isn't even checked by a compiler); how can I be sure that my proof doesn't contain bugs? Why would it make my program less error-prone? Is there any article that tries to compare heavy testing with FM?

On Sunday 14 September 2008 6:59:06 am Rafael Almeida wrote:

One thing have always bugged me: how do you prove that you have correctly proven something? I mean, when I write a code I'm formaly stating what I want to happen and bugs happen. If I try to prove some part of the code I write more formal text (which generally isn't even checked by a compiler); how can I be sure that my proof doesn't contain bugs? Why would it make my program less error-prone? Is there any article that tries to compare heavy testing with FM?

This isn't really a problem if you're programming in a language in which the proofs of program correctness are checked by the compiler/what have you, as Chaddaï has already said. In that case, it's similar to asking, "how do I know my Haskell programs are actually type correct?" Barring bugs in the tools (which, in the ideal case, are built on a simple enough foundation to be confidently proven correct by hand), it's not so much a concern. A more difficult question is: how do I know that the formal specification I've written for my program is the right one? Tools can fairly easily check that your programs conform to a given specification, but they cannot (to my knowledge) check that your specification says exactly what you want it to say. Of course, this is no worse than the case with test suites, since one can similarly ask, "how can I be sure the tests check for the properties/behavior that I actually want?" -- Dan

On Mon, 15 Sep 2008 10:32:44 -0400 Stefan Monnier wrote:

...

A more difficult question is: how do I know that the formal specification I've written for my program is the right one? Tools can fairly easily check that your programs conform to a given specification, but they cannot (to my knowledge) check that your specification says exactly what you want it to say.

The key is *redundancy*: as long as your property is sufficiently different (in structure, in authorship, etc...) you can hope that if the spec has a bug, the code will not have a corresponding bug and vice versa. It's only a hope, tho.

There are other meta-level properties one might desire in a specification, too, such as: * Simplicity - if a specification is too long-winded, you might not spot a bug in it because it's too hard to read. * Definite description - if a specification is a definite description, it is satisfied by one and only one value (up to functional equivalence). For example, if I say that a list sorting function must preserve the length of its input, that's not a definite description, because it is satisfied by the identity function, as well as a correct sorting function. However, if I say (in a suitably formal way) that a sorting function must output a list where every element in the input occurs the same number of times in the output as it occurs in the input, and vice-versa, and the output is ordered according to the specified order - then that *is* a definite description, because any two functions that follow that specification must be equivalent. * Reusable (and perhaps reused!) - As in ordinary programming, reuse of specifications can help avoid errors. -- Robin