I use interval arithmetic for reliable computing. Now, a procedure coded in a good implementation of interval arithmetic takes perhaps about eight times as much as the same procedure carried out without interval arithmetic (if the lion's share of runtime is taken by floating-point computations). I have sometimes been asked why I don't do rounding-error analysis by hand instead. To me, that does not look like a good option: it amounts to saving computer time at the expense of human time, and creates one more occasion for human error.

Now, what would make sense for me would be for there to be a system for bounding rounding errors with the help of a computer. It might not be realistic to expect a computer to analyse the total error in fairly complex procedures, but a human and a computer might be able to do a quicker and more reliable job than a human working alone, and produce a certificate of correctness to boot. (Cf. how it is much easier to produce a formal proof with computer assistance.)

Note: perhaps it shows, but -- I am a pure mathematician; feel free to tell me if what I say seems a little naïve.

  • $\begingroup$ Check out this and this. $\endgroup$ Aug 26, 2018 at 2:34
  • $\begingroup$ Thanks! I would be interested in how error analysis in the sense of e.g. Wilkinson could be used in the context of a rigorous proof. I could see how it might be possible to implement it by means of a system for the computer-aided production of formal proofs. Has such a thing been done in practice? $\endgroup$ Aug 26, 2018 at 6:30


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.