Is it possible to prevent arithmetic errors with a dependent type system?
In theory, you can do anything of this sort with dependent types! Typically you would define your own (dependent) type, say

b_int = {z : Z | MIN_INT &lt;= z &lt;= MAX_INT}


Depending on the "flavor" of your dependent types, you might need a bunch of functions for going from b_int to Z and vice-versa (for well-defined values).

and then your function f would have to be of type:

 f : b_int * ... * b_int -&gt; b_int


Now the tricky part. First you have to specify all the arithmetic operators, say b_add : b_int * b_int -&gt; b_int in terms of the "ordinary" add function add. Ah except this isn't quite right. b_add MAX_INT 1 shouldn't be allowed! So you would have to give it a stricter specification, along the lines of

 b_add : { (n, m) : b_int * b_int | MIN_INT &lt;= n + m &lt;= MAX_INT } -&gt; b_int


Then you want to prove something along the lines of:

b_add_correct : forall n m, n + m = b_add(n,m)


where the pair (n,m) needs to be in the domain of definition of b_add. Here, again, there may be a lot of pain if you need to translate to and from the Z type of unbounded integers, depending on how explicit the sub-types are.

Similarly for division:

b_div : { (n, m) | MIN_INT &lt;= n / m &lt;= MAX_INT, m =/= 0 }


So, if your program only uses the bounded operations, then there should be no way of writing a type correct program that has overflow or NaN operations.

However, I hope to convince you as well that there may be a significant amount of pain if there are no natural inclusions of types into sub-types, b_nat -&gt; Z and if proofs of the inequalities have to be carried around explicitly.

One example is if the coercion box : Z -&gt; b_nat explicitly carries the proof of inequality, i.e. box actually has the type:

 box : (x : Z) -&gt; (p : x &lt;= MAX_INT) -&gt; b_nat


(I'm omitting the lower bound for simplicity). Then the correctness for b_add might be something more like:

 b_add_correct : forall n m : Z, (p : n &lt;= MAX_INT) -&gt; 
                                 (q : m &lt;= MAX_INT) -&gt; 
                                 (r : n + m &lt;= MAX_INT) -&gt;
    n + m = unbox (b_add (box n p) (box m q) r)


Whew! It gets even worse if just applying a bop operation requires explicitly building a proof that some bound holds (for example if you know $n &lt; m$, then you might want to use the fact that $m - n \neq 0$ to do division). That can make your program look quite messy, and be hard to write, since your proof obligations and program writing become inextricably linked.