The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

Dear Yann,

Russell O'Connor has just completed a PhD-thesis on this topic:
http://www.r6.ca/thesis.pdf
It includes an introduction to numerical computations inside the Coq proof 
assistant.

Bas


On Friday 16 October 2009 12:07:04 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 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.