But that’s because null is a static type. Zero isn’t a static type. How can I know if a calculation produces zero if I can’t predict the result of it at compile time?
The problem is these checks can be rather slow and people don’t want to wait a long time for their type checking and analyzers to finish. But LLMs can both wait longer and by internalizing the logic can reduce the number of times it will need to trigger them.
Edit: I’ll need to examine this project to know where (or if) they draw the distinction between normal type checking and a post type check analyzer. If they blend the two and throw the whole thing into Z3 it’ll work but it’ll be needlessly slow.
Edit: What I’m calling a post type check anyalizer they’re calling a contract verifier and it’s a distinct stage with ‘check’ (type check) then ‘verify’ (Z3).
So, in pseudocode
int div(int a, int b): return a / b;
Would probably be a compile time error, but
int div(int a, int b): return b == 0 ? ERR : (a /b);
Would not, or at least that's what I'd expect.
The whole things looks vibe-coded, and vibe-designed.
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.
Or maybe it's over your head and you should just stick to reading children's fiction after all. Want some colouring books too?
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.