alt Hacker NewsThe issue I have with all these formally verified numerical algorithms is that, at the end of the day, I need this implemented using actual floating point. It's great that it's verified, but not for the case that is practically meaningful. Unless it's implemented using hardware accelerated floating point, most of these algorithms are not sufficiently performant to be practically useful.
Replies
There are plenty of proof systems that can handle floating point? The proof doesn't happen during execution...
> The issue I have with all these formally verified numerical algorithms is that, at the end of the day, I need this implemented using actual floating point.
You can go a very long way using discrete math though. I'm pretty sure it's doable to implement, say, a 3D slicer (to prepare layers/paths for 3D printing I mean) without using any floating point operation.
P.S: FWIW I was coding intros and demos using 3D effects on the Commodore Amiga and then on 386 PCs without using the 387 (the FP co-processor of the 386, when present). I'm not saying it's useful to play games in 4K: what I'm saying is that there are certainly applications where formally verified algos using integer math do make sense.
It is possible to prove things involving floats, you just have to addionally trust a small set of axioms on floats. See https://github.com/schildep/verified-3d-mesh-intersection#pe... Don't know if there is something like this in Lean. But there is https://flocq.gitlabpages.inria.fr