I have a very basic notion about interval arithmetic (IA), but it seems to be a very interesting branch of computational science both theoretically and practically. It is clear that the obvious applications are verified computing and ill-posed problems, but this is too abstract. Since there are a lot of people involved in applied computations here, I’m curious about real world problems which are hard or impossible to solve without IA.
This answer partly responds to JackPoulson's comment (because it is long), and partly answers the question.
Interval arithmetic is a computational procedure to give rigorous bounds on calculated quantities, only in the sense that the interval extension of a real-valued function over an interval encloses the image of that function over the same interval. Without calculating anything, interval arithmetic cannot give you any insight about what factors influence the numerical error in a calculation, whereas the theorems in Higham's book and others do give you insight into the factors influencing numerical error, at the cost of potentially weak bounds. Granted, the bounds obtained using interval arithmetic may also be weak, due to the so-called dependency problem, but sometimes they are much stronger. For instance, the interval bounds obtained using the integration package COSY Infinity are much tighter than the types of error bounds you would get on numerical integration from the results of Dahlquist (see Hairer, Wanner, and Nørsett for details); these results (I am particularly referring to Theorems 10.2 and 10.6 in Part I) give more insight into sources of error, but the bounds are weak, whereas the bounds using COSY can be tight. (They use several tricks to mitigate dependency issues.)
I hesitate to use the word "proof" when describing what interval arithmetic does. There are proofs involving interval arithmetic, but calculating results using interval arithmetic with outward rounding is really just a means of bookkeeping to conservatively bound the range of a function. Interval arithmetic calculations are not proofs; they are a way to propagate uncertainty.
As far as applications go, in addition to Stadtherr's work in chemical engineering, interval arithmetic has also been used to calculate bounds for particle beam experiments (see the work of Makino and Berz, linked to the COSY Infinity web site), they've been used in global optimization and chemical engineering design applications (among others) by Barton (the link is to a list of publications), the design of spacecraft and global optimization (among others) by Neumaier (again, the link is to a list of publications), global optimization and nonlinear equation solvers by Kearfott (another list of publications), and for uncertainty quantification (various sources; Barton is one of them).
Finally, a disclaimer: Barton is one of my thesis advisers.
Interval arithmetic gives you a proof with mathematical rigor.
Good examples of actual applications is the work of Mark Stadtherr and his research group. In particular, phase equilibrium and stability calculations are successfully solved with intervals methods.
A nice collection of benchmarks, with reference to their physical background, is at the ALIAS website.
Another feature of interval arithmetic and its generalizations is that it allows adaptive exploration of the domain of a function. It can thus be used for adaptive geometric modeling, processing, and rendering, just to take examples from computer graphics.
Interval methods have featured in some recent proofs of hard mathematical theorems such as the existence of chaos in the Lorenz attractor and the Kepler Conjecture. See http://www.cs.utep.edu/interval-comp/kearfottPopular.pdf for these and other applications.
Interval arithmetics is very useful for geometric algorithms. Such geometric algorithms take as input a set of geometric objects (e.g. a set of points) and construct a combinatorial data structure (e.g. a triangulation) based on spatial relations between the points. These algorithms depend on a small number of functions, called 'predicates', that take as input a fixed number of geometric objects and return a discrete value (typically one of 'above,aligned,below'). Such predicates typically correspond to the sign of a determinant of the point's coordinates.
Using standard floating-point numbers is not sufficient, since it may fail accurately compute the sign of the determinant, and even worse, return incoherent results (i.e., saying that A is above B AND B is above A, thus making the algorithm create a mess instead of a mesh !). Systematically using multi-precision (such as in the Gnu Multi-Precision library and its MPFR extension to multi-precision floating point numbers) works but causes a significant performance penalty. When the geometric predicate is the sign of something (as in most cases), using interval arithmetics allows one to do a faster computation, and then only launch the more expansive multi-precision computation if zero is in the interval.
Such an approach is used in several large computational geometry codes (e.g. CGAL).