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. 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.