Re: [isabelle] Numerical Recipes in Isabelle

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 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 !



P.S. I crosspost on the Coq and PVS mailing lists.

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