In your "never produce NaN" arithmetic, what do you want sqrt(-1) to be, and why is that a better answer than NaN?

I want it to throw an exception - a language-level exception - and I'm fine with sacrificing a bit of performance (i.e. checking the flags after every operation) to do so. This is a better answer because it means I see the error where it actually happened, rather than getting a NaN out the end of my calculation and having no idea which particular computation it came from.

This is what we had before IEEE-754. Instead of having a closed arithmetic system, exceptional conditions caused a trap (the "language-level exception" of its day). It was a terrible situation, and the direct cause of several "software-caused disasters" that you may have learned about in an engineering class.

Having division by zero being an unchecked exception is a terrible idea, as you say.

But that's not what I want. I want a paranoid language. I want a language where potential division by zero is a checked exception. One where "a = b / c" won't even compile if c might be 0. One that won't compile if it can find an example of an input to a function where an assertion fires. I want one where there is no such thing as an unchecked exception. Or rather, one where you can explicitly override checked exceptions to be the equivalent of (read: syntactic sugar for) "except: print(readable exception trace); exit(<code>)" - but you need to explicitly override it to do so.

Would it be a pain to write in? Yes. But at the same time there's a lot of software that would be best written in this manner. A language where the language itself forces you to be paranoid.

> One where "a = b / c" won't even compile if c might be 0.

Dependently typed languages can provide this.

Can you give an example? I have yet to run into a language that doesn't require a proof of correctness, but will just attempt to find a counterexample.

Well, it sounds like what you're looking for is property based testing. You can setup something like QuickCheck to run at compilation.

You need to provide a proof, but in e.g. Idris the language gives you the tools to make that proof quite easy.

[Citation needed]

Again: I am looking for a language that doesn't require you to provide a proof. I'm looking for a language that is a "logical extension" of what currently is available - that is, I am looking for a language that will attempt to find a counterexample on compilation and will bail if it can.

But non-exhaustively? That exists already - plenty of languages will warn or error if they can tell you're dividing by zero, but don't catch every possible case.

Any working program will in some sense be a proof, by Curry-Howard. So I think asking to not have to provide a proof is backwards; what you want is a language that makes it easy to express the program and manipulate it as a proof.

Only because of inadequate language support (or, in the case of that Ariane 5, deliberately overriding the language support)

I know that's what a lot of people want, but I do not see how one can 'handle the extremes in reasonable ways' without producing NaNs. I have heard people advocate 0/0 = 0, but IMO that is NOT 'handling the extremes in reasonable ways'. What would you propose for 0/0?

More than that, a signaling NaN should raise an exception if used in a comparison. Otherwise, you get a bogus comparison and a bogus branch.

It isn't possible to never produce a NaN. 0/0 and inf-inf, for example, have no reasonable result that can be produced. And indeed, the spec defines those operations as resulting in NaN.