Other answers have already considered the relative merits of your ideas. I propose another one: use basic flow analysis to determine whether a variable can be zero. Then you can simply disallow division by variables that are potentially zero.
x = ... y = ... if y ≠ 0: return x / y // In this block, y is known to be nonzero. else: return x / y // This, however, is a compile-time error. Alternatively, have an intelligent assert function that establishes invariants:
x = ... require x ≠ 0, "Unexpected zero in calculation" // For the remainder of this scope, x is known to be nonzero. This is as good as throwing a runtime error—you skirt undefined operations entirely—but has the advantage that the code path need not even be hit for the potential failure to be exposed. It can be done much like ordinary typechecking, by evaluating all branches of a program with nested typing environments for tracking and verifying invariants. It also:
x = ... // env1 = { x :: int } y = ... // env2 = env1 + { y :: int } if y ≠ 0: // env3 = env2 + { y ≠ 0 } return x / y // (/) :: (int, int ≠ 0) → int else: // env4 = env2 + { y = 0 } ... ... // env5 = env2 Furthermore, it extends naturally to range checking,and null checking, &c. if your language has such features.