Re: [isabelle] Numerical Recipes in Isabelle



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.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.