> Of course there's no way to tell at compile time that a value will definitely be zero.

Yes there is. Dependently typed languages like Idris can inspect terms at the value-level during compile time. Rather, instead of proving that the divisor will be zero, you must instead statically prove that the divisor cannot be zero; otherwise the code will not typecheck.

Okay,

int integer_division(int a, int b) { if (b!=0) return a/b; raise(SIGFPE); }

Great.