Formally verifying a floating-point division routine with Gappa – part 1 (opens in new tab)

Usually when I read posts like this, I come out with wonder and thinking "what amazing tools there are in our world". This time, however, my opinion is that Gappa is too raw to use effectively yet

Sure, some of the problems encountered are due to different domain (it might not have been expected that math-oriented tool would be checking code, so it's no surprise that in the end the author's mistake was found in translation _into_ math form). But others feel straight up unfinished

"no evaluate() mode" and "no output of intermediates" indicates that dev hasn't encountered varied enough early adopters yet (to learn that such a UX is needed for manual optimization)

"needs (q+e)-Q==(q-Q)+e hint" means there are some gaps yet to be filled in the implementation or the manual

and "output more than 1 value for 1-value input range" seems straight up as a bug

---

in the end it seems like a nice idea - but I'll be waiting for one more blog down the line before putting Gappa into my toolbelt

A very interesting read.

The article states that they added a computational correction step which is run whenever a result might be incorrect but skip it most of the time.

I am wondering whether this might cause problems for small real-time systems that do not have an FPU. If the runtime cost of an operation depends on the input, it is very hard to figure out whether deadlines can be met in all operation conditions.

I love this type of articles with mix of math and algorithms. I intuitively thought that one can just use a pair of float divisions, like with addition or multiplication.

Oh, and I hope this algorithm can be used to improve RISC-V.