See https://www.cl.cam.ac.uk/~jrh13/papers/thesis.html for your question, John Harrison got a job with Intel based on this after their floating point disaster.
But in short: theorem proving is not about equalities, it is about inequalities. And theorems about numerical algorithms are a great example of this.
See https://www.cl.cam.ac.uk/~jrh13/papers/thesis.html for your question, John Harrison got a job with Intel based on this after their floating point disaster.
But in short: theorem proving is not about equalities, it is about inequalities. And theorems about numerical algorithms are a great example of this.