Re: [isabelle] Numerical Recipes in Isabelle



Hi,

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 ?

this is possible in Isabelle, though it might be a little bit harder and cumbersome than you might imagine and the resulting code is not as efficient as you would like it to be :-) Recently there has been work on computing with floating point numbers in Isabelle, and stuff like Taylor-approximation is available now, I think (though I do not know how accessibly packaged this is). There is one efficiency problem: To my knowledge sabelle does not directly deal with the usual IEEE floats and doubles, but uses a pair of arbitrary size integers to encode a float. This and the fact that your code will be functional code (as opposed to imperative code) will make the compiled code way slower than if coded for example in C.

Cheers,

Steven Obua







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