3 ms·

> Division by zero is not a runtime error — it is a type error. The compiler checks every call site to prove the divisor is non-zero. Elaborate a little here.

hgoel 5mo ago
Presumably an analyzer that makes it an error to not have an immediately traceable zero check. C# can do something similar with null references. It can require you to indicate which arguments and variables are capable of being null, and then compiler error/warning if you pass it to something that expects a non-null reference without a null check.
- hyperhello 5mo ago
  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?
  - hgoel 5mo ago
    I think it's about if there's a possibility of it being zero. Of course there's no way to tell at compile time that a value will definitely be zero. 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.
    - still_grokking 5mo ago
      Or it's just some AI brain fart… The whole things looks vibe-coded, and vibe-designed.
    - rdevilla 5mo 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.
      - hyperhello 5mo ago
        Okay, int integer_division(int a, int b) { if (b!=0) return a/b; raise(SIGFPE); } Great.
        rdevilla 5mo ago
        You don't appear to understand the difference between runtime and static analysis/compile time, or term-level and type-level.
        hyperhello 5mo ago
        Great! Explain it to us while I read to my kid!
        cjbgkagh 5mo ago
        The ‘let me google that for you’ is set to be replaced with ‘let me ask ChatGPT for you’.
        rdevilla 5mo ago
        Don't get mad because you're too lazy to even ask the AI. You are first to be replaced in the workforce. Or maybe it's over your head and you should just stick to reading children's fiction after all. Want some colouring books too?
        hyperhello 5mo ago
        Yes! We can always use more books and toys here!
        imtringued 5mo ago
        This is a very antagonistic comment. Some people would call it "passive aggressive". 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.
  - cjbgkagh 5mo ago
    Post type check analyzers can work with more than just the type information, you can really do whatever you want at this stage. The normal highly optimized type checker handles the bulk of the checking and the post type check analyzers can work on the residual. You wouldn’t type check a file that doesn’t parse, and you wouldn’t run the analyzers on code that doesn’t type check. 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).

hgoel 5mo ago

Presumably an analyzer that makes it an error to not have an immediately traceable zero check. C# can do something similar with null references. It can require you to indicate which arguments and variables are capable of being null, and then compiler error/warning if you pass it to something that expects a non-null reference without a null check.

hyperhello 5mo ago
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?
- hgoel 5mo ago
  I think it's about if there's a possibility of it being zero. Of course there's no way to tell at compile time that a value will definitely be zero. 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.
  - still_grokking 5mo ago
    Or it's just some AI brain fart… The whole things looks vibe-coded, and vibe-designed.
  - rdevilla 5mo 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.
    - hyperhello 5mo ago
      Okay, int integer_division(int a, int b) { if (b!=0) return a/b; raise(SIGFPE); } Great.
      - rdevilla 5mo ago
        You don't appear to understand the difference between runtime and static analysis/compile time, or term-level and type-level.
        hyperhello 5mo ago
        Great! Explain it to us while I read to my kid!
        cjbgkagh 5mo ago
        The ‘let me google that for you’ is set to be replaced with ‘let me ask ChatGPT for you’.
        rdevilla 5mo ago
        Don't get mad because you're too lazy to even ask the AI. You are first to be replaced in the workforce. Or maybe it's over your head and you should just stick to reading children's fiction after all. Want some colouring books too?
        hyperhello 5mo ago
        Yes! We can always use more books and toys here!
        imtringued 5mo ago
        This is a very antagonistic comment. Some people would call it "passive aggressive". 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.
- cjbgkagh 5mo ago
  Post type check analyzers can work with more than just the type information, you can really do whatever you want at this stage. The normal highly optimized type checker handles the bulk of the checking and the post type check analyzers can work on the residual. You wouldn’t type check a file that doesn’t parse, and you wouldn’t run the analyzers on code that doesn’t type check. 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).