*To*: Tobias Nipkow <nipkow at in.tum.de>*Subject*: Re: [isabelle] Numerical Recipes in Isabelle*From*: Amine Chaieb <ac638 at cam.ac.uk>*Date*: Tue, 20 Oct 2009 18:51:36 +0200*Cc*: Yann Le Du <yledu at free.fr>, Isabelle <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <4ADAF6BC.6060205@in.tum.de>*References*: <e1cb29bb0910160318j68f8ddadqfb56ed3349bc4192@mail.gmail.com> <4ADAF6BC.6060205@in.tum.de>*Sender*: Amine Chaieb <chaieb.amine at googlemail.com>*User-agent*: Thunderbird 2.0.0.23 (X11/20090817)

You might be interested in previous considerations such as described in this paper: http://citeseer.ist.psu.edu/old/535034.html Theorem provers are not mentioned there though. Note also that functional programming does not necessarily mean less efficiency. Purely functional programs are highly parallelizable and if your target programming language already provides parallel implementations of some key-functions like map, fold_map etc... then you can extract parallel code for free. This has been done for ML see for that e.g. Makarius's latest work (http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf). Haskell also provides one of the best parallelization architectures, hopefully Ocaml will follow soon. One further point worth mentioning here is when it worth the effort to verify/implement numerical algorithms in a theorem prover? In several cases, it will just be sufficient to check the results. Take for example the simple problem of LU decomposition of a matrix. All you need is to compute *somehow* L and U, then check that L is upper triangular and U is lower diagonal (very easy), and that the product is your original matrix. The algorithm itself need not be verified, just the results (but here again, each time!!). The same applies to several other problems like interpolation, root finding (depending on what you want to verify), Eigenvalues etc... In some cases you will need to implement and verify the full algorithm of course. I don't see for instance a simple check for numerical integration. Amine. Tobias Nipkow wrote: > There is something else you have to beware of: purely functional > languages do not have mutable arrays! Of course you can simulate them by > lists, but the resulting code is very inefficient. Different languages > and provers have different answers to this. The Isabelle answer is the > Haskell answer: you need to write your code in a monadic style, then > Isabelle and later the Haskell compiler can generate code that updates > arrays in place. > > Tobias > > 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

**Re: [isabelle] Numerical Recipes in Isabelle***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] haskabelle importer
- Next by Date: [isabelle] haskabelle syntax check
- Previous by Thread: Re: [isabelle] Numerical Recipes in Isabelle
- Next by Thread: [isabelle] haskabelle importer
- 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