| ▲ | quanto 5 hours ago | |
> 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? | ||
| ▲ | thesmtsolver 4 hours ago | parent | next [-] | |
There is nothing inherently difficult about practical implementations of continuous numbers for automated reasoning compared to more discrete mathematical structures. They are handleable by standard FOL itself. See ACL2's support for floating point arithmetic. https://www.cs.utexas.edu/~moore/publications/double-float.p... SMT solvers also support real number theories: https://shemesh.larc.nasa.gov/fm/papers/nfm2019-draft.pdf Z3 also supports real theories: | ||
| ▲ | kragen 4 hours ago | parent | prev [-] | |
I'm curious about how you'd do that, too. I haven't tried doing anything like that, but I'd think you'd start by trying to formalize the usual optimality proof for the Kalman filter, transfer it to actual program logic on the assumption that the program manipulates real numbers, try to get the proof to work on floating-point numbers, and finally extract the program from the proof to run it. https://youtu.be/_LjN3UclYzU has a different attempt to formalize Kalman filters which I think we can all agree was not a successful formalization. | ||