Hacker News new | ask | show | jobs
by sjrd 480 days ago
We actually proved correctness of the fast Long division of Scala.js using similar reasoning. [1] We had mechanical proofs for the other operations, but the solver couldn't handle division. The interplay between bit vector semantics and floating point semantics was too much for it to bear.

Scala.js has the fastest implementation of 64-bit integers on the JavaScript engine. The implementations cannot be understood unless you actually prove them correct. IMO that's one of the best reasons to invest in the formal proof of a program fragment.

[1] https://lampwww.epfl.ch/~doeraene/thesis/doeraene-thesis-201... section 4.4.2, page 114.
1 comments
copperx 480 days ago
> The implementations cannot be understood unless you actually prove them correct

I quickly scanned the book you provided, but I couldn't find an explanation.

What do you mean by 'understood'?

link