> when I can get away with it I'd prefer to prove things with real numbers and assume magically they transfer to floating point.
True for some approaches, but numerical analysis does account for machine epsilon and truncation errors.
I am aware that Inria works with Coq as your link shows. However, the link itself does not answer my question. As a concrete example, how would you prove an implementation of a Kalman filter is correct?
True for some approaches, but numerical analysis does account for machine epsilon and truncation errors.
I am aware that Inria works with Coq as your link shows. However, the link itself does not answer my question. As a concrete example, how would you prove an implementation of a Kalman filter is correct?