12
$\begingroup$

I have implemented (in TeX, but it doesn't matter for this question) a library of functions that evaluate basic arithmetic, as well as some transcendental functions such as cosine, on decimal floating point numbers with a certain range of exponents and digits in the mantissa. It may be good to prove some formal guarantees on the maximum error when rounding, and the lack of overflow.

Which tool (proof assistant and library) can I use to efficiently prove that certain manipulations of strings of digits will indeed compute a (suitably rounded) sum or product of floating point numbers.

For instance, I have heard that Coq provides some way to prove correctness of some binary floating point functions, but I am more interested in decimal arithmetic.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
6
$\begingroup$

If you have implemented "a library of functions that evaluate basic arithmetic, as well as some transcendental functions such as cosine, on decimal floating point numbers" and you want to test its correctness, then the most accurate, fast, easy, and overall efficient way to do this would be to compare its results to something like the mpmath library in Python which is free and open-source and can handle arbitrary-precision arithmetic.

If you want to insist on using a proof assistant to do this, then I'll say that most proof assistants (Coq, Lean, etc.) can theoretically do it, but it would be more laborious for you and surely it would be slower for accomplishing the task of verifying the accuracy of your floating-point arithmetic!

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ In fact, I already have a test suite comparing the outputs of my code to the expected ones for a small number of inputs (say, 100), but this cannot easily detect mistakes like overflows in intermediate calculations, or threshold effects when different formulas are used for different ranges of arguments (e.g., upon argument reduction in cosine). That said, +1 because it is a good idea to look beyond proof assistants for this kind of tasks, as a first defense against bugs. $\endgroup$
    – Bruno Le Floch
    Feb 10, 2022 at 20:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.