Numerical Recipes in Coq

[Yann Le Du-5]

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 Coq, 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 Coq (if that has any meaning) ? How would a software engineer approach the task of coding Numerical Recipes ? Since Coq can extract Haskell/OCaml code, then am I right to envision a "proved correct" Coq 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 will crosspost on the Isabelle and PVS mailing lists.

[Bas Spitters]

Dear Yann,

Russell O'Connor has just completed a PhD-thesis on this topic:
http://www.r6.ca/thesis.pdf
It includes an introduction to numerical computations inside the Coq proof
assistant.

Bas


On Friday 16 October 2009 12:07:04 Yann Le Du wrote:

> 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 Coq, 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 Coq (if that
> has any meaning) ? How would a software engineer approach the task of
> coding Numerical Recipes ? Since Coq can extract Haskell/OCaml code, then
> am I right to envision a "proved correct" Coq 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 will crosspost on the Isabelle and PVS mailing lists.

--------------------------------------------------------
Bug reports: http://logical.saclay.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club