*To*: Yann Le Du <yledu at free.fr>*Subject*: Re: [isabelle] Numerical Recipes in Isabelle*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Sat, 17 Oct 2009 15:25:36 +0200*Cc*: Isabelle <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <e1cb29bb0910160318j68f8ddadqfb56ed3349bc4192@mail.gmail.com>*References*: <e1cb29bb0910160318j68f8ddadqfb56ed3349bc4192@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.23 (Macintosh/20090812)

Dear Yann, A logical account of Numerical Recipes can take on two distinct forms: 1. You give up on imperative programming, use the prover's built-in functional language, and extract functional code at the end. 2. You write C code and use some C verification tool that generates proof obligations that you prove with your favourite prover. Option 1 seems to be what you have in mind, which is why I will concentrate on it. It is the most direct approach and usually leads to simpler proofs. Note that I have not refered explicitly to any particular prover. Option 1 is viable with Coq, Isabelle and PVS. There are some variations on this approach, eg in Isabelle you could write your code in Haskell and import it to Isabelle for verification, which may appeal to the programmer, but most of the work would still be at the Isabelle level. Is your task advisable? It should enable you to do some very interesting research on the theorem proving front. Whether you will convince your community is another matter. Because, make no mistake, these proofs are hard to push through any prover. You will not be able to just breeze through Numerical Recipes and tick off one algorithm after another. For example, you will often have to establish quite a bit of background maths first that the prover does not know about. And unless you find bugs, the response to a successful verification of a well-known algorithm is likely to be muted on the application front. How would a software engineer approach the task of coding Numerical Recipes? He would draw a UML class diagram in his favourite case tool and generate the code automatically ;-) Best Tobias PS You should also look at HOL Light http://www.cl.cam.ac.uk/~jrh13/hol-light/. It does not directly support generation of OCaml code (although it could) but has a first-rate mathematics library (which we are in the process of importing to Isabelle). Yann Le Du schrieb: > Dear all, > > Benjamin Pierce, who suggested I should send the question that follows on > this mailing list, writes, in the introduction to his new book on "Software > Foundations", that "logic is to software engineering what calculus is to > mechanical/civil engineering". Now that caught my attention since, as a > physicist who recently discovered the world of formal methods thanks to > Dijkstra's archives, I believe formal methods (program derivation, proof of > correctness, etc.) can help me in my work in physics for which I code > different kinds of things including simulations and solvers. Now, following > Pierce, how could I "logicize" my coding ? > > I'm very ignorant of Isabelle, I just read the back cover blurb, but let me > go to the heart of the matter : is it possible, and advisable if we want to > do things correctly, to code Press et al. "Numerical Recipes" in Isabelle > (if that has any meaning) ? How would a software engineer approach the task > of coding Numerical Recipes ? Since Isabelle, like Coq if I'm not mistaken, > can extract Haskell/OCaml code, then am I right to envision a "proved > correct" Isabelle numerical recipe then extracted to Haskell/Ocaml and > efficiently compiled ? > > The answer to that central question determines the fate of many others I > have in store ! > > Sincerely, > > Yann > > P.S. I crosspost on the Coq and PVS mailing lists.

**References**:**[isabelle] Numerical Recipes in Isabelle***From:*Yann Le Du

- Previous by Date: Re: [isabelle] Numerical Recipes in Isabelle
- Next by Date: Re: [isabelle] Numerical Recipes in Isabelle
- Previous by Thread: Re: [isabelle] Numerical Recipes in Isabelle
- Next by Thread: Re: [isabelle] Numerical Recipes in Isabelle
- Cl-isabelle-users October 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list