One of these days I'll get around to Rust. I don't think it's fundamentally difficult, just different from most people's cowboy programming. I'm much more excited these days about program extraction from verified programs written in Idris or Coq, which is on a whole other level of pain and suffering.
Mind you even correctness checkers aren't panacea - they won't go all the way down to check if you are using IEEE 754 correctly and handle all possible edge cases and rather assume "well-defined math properties". And as Donald Knuth used to say: "Beware of bugs in the above code; I have only proved it correct, not tried it."
Numeric 'correctness' is a business-problem property.
For a game engine, correctness is speed and "right enough". For a research physics simulation, it may be "as right as possible".
You can't check whether floating point inaccuracy is correct generically because the definition is entirely dependent on the business needs of the program in question.
