Parse, don't Validate and Type-Driven Design in Rust

"Parse, don't Validate" and encoding validation information into the type system is an extremely valuable technique.

But division by zero is the perfect example of a use case where encoding validation into the type system is unlikely to work.

If we were reading in numbers from a file, it might be useful to verify that some of them are non-zero at the point where we read them in. But that's not where we typically get numeric values: we typically get them from other computations. Sure, there are a few specialized circumstances where we can propagate validation information using the type system: adding or multiplying two StrictlyPositive values can be guaranteed to return another StrictlyPositive value. But in most cases we care about, that doesn't work. Subtracting two different StrictlyPositive values does not guarantee to return something that is non-zero. Adding two different NonZero values is not guaranteed to give another NonZero.

The point of all that, is that assuming your denominators come as the result of other computation, you probably can't perform a check at the very beginning of the computation and let the type checker enforce it from there. Instead, you have to check whether a value is zero. Immediately before performing the division. That's not actually any safer! You get an error, one step earlier, but you have done nothing to fundamentally reduce the number of places in your code where an error could potentially occur!

In contrast, the solution that is built into floating point numbers actually DOES reduce the number of places in your code that you must check for an error. Perform the computation, potentially dividing by zero at quite a few different points. Then, just once (at the end of the computation) check to see whether you have NAN. Because NAN is "infectious", you can be confident of catching the issue (although, unfortunately, you catch it after the fact rather than beforehand).