Email Gateway (Aug 18 2022 at 14:12): Email Gateway (Aug 18 2022 at 14:12):From: Yann Le Du <yledu@free.fr>
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.
Email Gateway (Aug 18 2022 at 14:12):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Yann,
A logical account of Numerical Recipes can take on two distinct forms:
You give up on imperative programming, use the prover's built-in
functional language, and extract functional code at the end.
You write C code and use some C verification tool that generates
proof obligations that you prove with your favourite prover.
Option 1 seems to be what you have in mind, which is why I will
concentrate on it. It is the most direct approach and usually leads to
simpler proofs.
Note that I have not refered explicitly to any particular prover. Option
1 is viable with Coq, Isabelle and PVS. There are some variations on
this approach, eg in Isabelle you could write your code in Haskell and
import it to Isabelle for verification, which may appeal to the
programmer, but most of the work would still be at the Isabelle level.
Is your task advisable? It should enable you to do some very interesting
research on the theorem proving front. Whether you will convince your
community is another matter. Because, make no mistake, these proofs are
hard to push through any prover. You will not be able to just breeze
through Numerical Recipes and tick off one algorithm after another. For
example, you will often have to establish quite a bit of background
maths first that the prover does not know about. And unless you find
bugs, the response to a successful verification of a well-known
algorithm is likely to be muted on the application front.
How would a software engineer approach the task of coding Numerical
Recipes? He would draw a UML class diagram in his favourite case tool
and generate the code automatically ;-)
Best
Tobias
PS You should also look at HOL Light
http://www.cl.cam.ac.uk/~jrh13/hol-light/. It does not directly support
generation of OCaml code (although it could) but has a first-rate
mathematics library (which we are in the process of importing to Isabelle).
Yann Le Du schrieb:
Email Gateway (Aug 18 2022 at 14:12):From: Steven Obua <obua@wjpserver.cs.uni-sb.de>
Hi,
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
Email Gateway (Aug 18 2022 at 14:12):From: Richard Waldinger <waldinger@AI.SRI.COM>
Pierce is paraphrasing John McCarthy:
Email Gateway (Aug 18 2022 at 14:12):From: Tobias Nipkow <nipkow@in.tum.de>
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).
Very nicely.
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.
Generating code with floats and doubles is not an issue. Of course you
need a theory of IEEE 754 to base your verification on. There are some
in HOL (which would not be hard to port to Isabelle).
You avoided machine floats because you wanted to rely on as few trusted
components as possible (which is the Coq/HOL/Isabelle tradition). But
for Numerical Recipes this would be unnatural and would appear esoteric
to that community.
Tobias
Email Gateway (Aug 18 2022 at 14:12):From: Tobias Nipkow <nipkow@in.tum.de>
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.
Tobias
Yann Le Du schrieb:
Email Gateway (Aug 18 2022 at 14:12):From: Amine Chaieb <ac638@cam.ac.uk>
You might be interested in previous considerations such as described in
this paper:
http://citeseer.ist.psu.edu/old/535034.html
Theorem provers are not mentioned there though.
Note also that functional programming does not necessarily mean less
efficiency. Purely functional programs are highly parallelizable and if
your target programming language already provides parallel
implementations of some key-functions like map, fold_map etc... then you
can extract parallel code for free. This has been done for ML see for
that e.g. Makarius's latest work
(http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf). Haskell
also provides one of the best parallelization architectures, hopefully
Ocaml will follow soon.
One further point worth mentioning here is when it worth the effort to
verify/implement numerical algorithms in a theorem prover? In several
cases, it will just be sufficient to check the results. Take for example
the simple problem of LU decomposition of a matrix. All you need is to
compute somehow L and U, then check that L is upper triangular and U
is lower diagonal (very easy), and that the product is your original
matrix. The algorithm itself need not be verified, just the results (but
here again, each time!!). The same applies to several other problems
like interpolation, root finding (depending on what you want to verify),
Eigenvalues etc...
In some cases you will need to implement and verify the full algorithm
of course. I don't see for instance a simple check for numerical
integration.
Amine.
Tobias Nipkow wrote:
Last updated: Apr 30 2024 at 04:19 UTC