Comment by rdevilla
15 hours ago
> 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.
No. In this type of language, the typical division function does not check against zero. It has a precondition that requires the caller to ensure that the divisor is not zero. If the data the caller has is completely arbitrary, then yes, the caller must use an if statement or similar. If the caller knows something about its data and can be sure that the divisor is not zero, then it doesn't need to use an if statement. But it might need to convince the proof checker that it knows what it's doing.
You don't appear to understand the difference between runtime and static analysis/compile time, or term-level and type-level.
Great! Explain it to us while I read to my kid!
4 replies →