Re: [isabelle] Numerical Recipes in Isabelle

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.


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.