*To*: Yann Le Du <yledu at free.fr>*Subject*: Re: [isabelle] Numerical Recipes in Isabelle*From*: Richard Waldinger <waldinger at AI.SRI.COM>*Date*: Sat, 17 Oct 2009 09:06:15 -0700*Cc*: Isabelle <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <e1cb29bb0910160318j68f8ddadqfb56ed3349bc4192@mail.gmail.com>*References*: <e1cb29bb0910160318j68f8ddadqfb56ed3349bc4192@mail.gmail.com>

Pierce is paraphrasing John McCarthy:

It is reasonable to hope that the relationship between computation and mathematical logic will be as fruitful in the next century as that between analysis and physics in the last. The development of this relationship demands a concern for both applications and mathematical elegance.

A Basis for a Mathematical Theory of Computation, 1963 On Oct 16, 2009, at 3:18 AM, Yann Le Du wrote:

Dear all,Benjamin Pierce, who suggested I should send the question thatfollows onthis mailing list, writes, in the introduction to his new book on"SoftwareFoundations", that "logic is to software engineering what calculusis tomechanical/civil engineering". Now that caught my attention since,as aphysicist who recently discovered the world of formal methodsthanks toDijkstra's archives, I believe formal methods (program derivation,proof ofcorrectness, etc.) can help me in my work in physics for which I codedifferent kinds of things including simulations and solvers. Now,followingPierce, how could I "logicize" my coding ?I'm very ignorant of Isabelle, I just read the back cover blurb,but let mego to the heart of the matter : is it possible, and advisable if wewant todo things correctly, to code Press et al. "Numerical Recipes" inIsabelle(if that has any meaning) ? How would a software engineer approachthe taskof coding Numerical Recipes ? Since Isabelle, like Coq if I'm notmistaken,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 manyothers Ihave 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: [isabelle] haskabelle importer
- 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