[helltone]

I dream of a programming language where I would be able to specify a computation and maybe error bounds on input/output and get efficient code respecting the bounds automatically. Arb takes us close to that, but I still have to handle recomputing with greater precision by hand, and things get complicated with multiple inputs. What are your thoughts on making arbitrary precision/rigorous error bounds more ergonomic to use for programmers?

[fdej]

That's a great question. Of course, you can express the computation as a function or a symbolic expression and evaluate it using a function that recomputes with greater precision automatically (or automatically compiles efficient code with bounds). Integrating this kind of functionality into the core semantics of a programming language is a very interesting problem.