[helltone]

I think perhaps this could be done in other ways that don't require interval arithmetic for autodiff, only that the gradient is conservatively computed, in other words carrying the numerical error from f into f'

[fph]

But the only way we know how to make "conservative computations" is via interval arithmetic.

[helltone]

No? Or maybe I'm missing something. If the goal is to be able to bound the computation of f, you can:

1) compute f with interval arithmetic

2) compute f normally and f' with interval arithmetic

3) compute f rounding towards zero, compute f' from f rounded towards infinity, and round f' up (if f positive) or round f' down (if f negative).

In all 3 cases you can use what you computed to figure out bounds on f, (1) is direct, the other two need extra work.