You're kind of saying the only way to do it is in software or hardware :)

An alternative https://en.wikipedia.org/wiki/Projectively_extended_real_lin...

The projectively extended real line defines division by zero, no reason you couldn't have a floating point type that implemented it.

>There's no viable way to statically prove at compile-time that these variables will never become zero at runtime

strongly typed programming languages like Ada allow for types which have ranges such as disallowing zero -- but also any arbitrary thing like you can create a floating point "degrees" type which is [0.0, 360.0] or any other ranged type