[FlipperBucket]

> the many pieces of code that assume that (x / y) * y equals x

The same issue if division by zero throws an exception. This is simply a more practical approach that dispenses with the exception handling (ie becomes a less irregular test case). Edit: Not buggy behavior, when expected.

[Jaxan]

I would say an exception is much more convenient. Buggy code that silently continues to run is very hard to debug!

[cousin_it]

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.

[seanmcdirmid]

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.

[cousin_it]

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

[dan-robertson]

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.

[cryptonector]

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

[antidesitter]

Can you elaborate?

[nanimo]

It's common to think of an exception as the program stopping and never being started again. In that sense, the invariant is still maintained, because the program never sees it violated. This has non-trivial consequences - for example, Rust lets exceptions and endless loops produce any value at all, even though they obviously can't actually do that.

[lmm]

Assuming an exception is equivalent to any non-exceptional value doesn't break anything. See "Fast and Loose Reasoning is Morally Correct".

[sclv]

Holy moly that is not at all what that paper says! It specifically argues that certain equational properties of a given total language continue to hold in the total fragment of a given partial language. It is an embedding theorem combined with lifting properties, not a license to perform _any_ reasoning at all regarding the non-total portion of the language it considers!