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.
int integer_division(int a, int b) { if (b!=0) return a/b; raise(SIGFPE); }
Great.
Dude, if you're reading to your kid you're clearly busy doing something else. No matter how simple the concept is, if you don't pay attention you're not going to get it so it's a failure on your part and not a failure on the part of the person patiently trying to explain something to you.
Or maybe it's over your head and you should just stick to reading children's fiction after all. Want some colouring books too?