On Oct 5, 2021, at 5:05 PM, Raffaello Giulietti <github.com+70726043+rgiulie...@openjdk.java.net<mailto:github.com+70726043+rgiulie...@openjdk.java.net>> wrote:
The proof of the central theorem of Schubfach is based on continued fractions. It was prepared on ACL2 by the late Dmitry Nadezhin, who was a member of Oracle's formal verification group. Dmitry also knew my writing inside-out: not a formal peer review but perhaps even more insightful. Dmitry (Dima) was excellent and made a number of fine contributions to Java core-libs math. Here is something he posted a few years back about formal checking of the contribution here under discussion: https://mail.openjdk.java.net/pipermail/core-libs-dev/2018-September/055768.html Schubfach has been exhaustively tested on all 2^32 floats, with approximations of powers of 10 of 63 bits each, rather than the full 126 bits used for doubles (the minimum size for doubles is 123 bits). It has also been tested for months on doubles, accumulating several trillions of witnesses and no failure. The exhaustive test on floats is an optionally executed part of the contributed code. I have run the exhaustive 32-bit test myself without seeing any errors. I also ran a 64-bit round trip test for probably at least a week without seeing any failures. I don’t know whether it has been mentioned in this recent thread as yet, but the performance of Schubfach is also much better then the JDK implementation, although I can’t recall with certainty the improvement. I think however that it was something like 14X? Brian
