Curry-Howard is not needed for theorem proving, it's just that type theorists like it.

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.