I used to think the same way: let's throw an exception on divide by zero, and forget NaN like a bad dream! But then someone explained to me that it's common to feed a billion numbers into a long calculation, then look at the results in the morning and find them okay, apart from a few NaNs. If each NaN led to an exception, you'd come back in the morning and find that your program has stopped halfway through. So there's a certain pragmatism to having numeric code silently continue by default.

Typically, divide by zero throws for integers because they can’t express NaN, which can instead be returned for floating point. In any case, integers can’t express special values, so you get exceptions instead. And this is actually defined at the processor level (for x86 among others), the trap is free (well, a sunk cost), why not take it?

Zero is not a very good NaN.

Yeah, agreed. The thing with 1/0=0 is bizarre, I guess my comment was more about why NaNs are okay.

What of a language without exceptions? A correct program can not assume that (x / y) * y = x because such an equality does not hold in general. Therefore the program must do something right in the case that y is zero before it tries dividing x by y to be correct. It shouldn’t really matter what x / 0 is because if a program relies on its value then it is probably wrong.

It's not convenient at all in a language like Coq.

Can you elaborate?