The Coq mailing list

[Yann Le Du <yledu AT free.fr>]

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.