Re: [isabelle] Numerical Recipes in Isabelle
go to the heart of the matter : is it possible, and advisable if we
do things correctly, to code Press et al. "Numerical Recipes" in
(if that has any meaning) ? How would a software engineer approach
of coding Numerical Recipes ? Since Isabelle, like Coq if I'm not
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and