4 ms·

This is what we had before IEEE-754. Instead of having a closed arithmetic system, exceptional conditions caused a trap (the "language-level exception" of its

This is what we had before IEEE-754. Instead of having a closed arithmetic system, exceptional conditions caused a trap (the "language-level exception" of its day). It was a terrible situation, and the direct cause of several "software-caused disasters" that you may have learned about in an engineering class.

lmm 12y ago
Only because of inadequate language support (or, in the case of that Ariane 5, deliberately overriding the language support)
TheLoneWolfling 12y ago
Having division by zero being an unchecked exception is a terrible idea, as you say. But that's not what I want. I want a paranoid language. I want a language where potential division by zero is a checked exception. One where "a = b / c" won't even compile if c might be 0. One that won't compile if it can find an example of an input to a function where an assertion fires. I want one where there is no such thing as an unchecked exception. Or rather, one where you can explicitly override checked exceptions to be the equivalent of (read: syntactic sugar for) "except: print(readable exception trace); exit(<code>)" - but you need to explicitly override it to do so. Would it be a pain to write in? Yes. But at the same time there's a lot of software that would be best written in this manner. A language where the language itself forces you to be paranoid.
- pseudonom- 12y ago
  > One where "a = b / c" won't even compile if c might be 0. Dependently typed languages can provide this.
  - TheLoneWolfling 12y ago
    Can you give an example? I have yet to run into a language that doesn't require a proof of correctness, but will just attempt to find a counterexample.
    - lmm 12y ago
      You need to provide a proof, but in e.g. Idris the language gives you the tools to make that proof quite easy.
      - TheLoneWolfling 12y ago
        [Citation needed] Again: I am looking for a language that doesn't require you to provide a proof. I'm looking for a language that is a "logical extension" of what currently is available - that is, I am looking for a language that will attempt to find a counterexample on compilation and will bail if it can.
        lmm 12y ago
        But non-exhaustively? That exists already - plenty of languages will warn or error if they can tell you're dividing by zero, but don't catch every possible case. Any working program will in some sense be a proof, by Curry-Howard. So I think asking to not have to provide a proof is backwards; what you want is a language that makes it easy to express the program and manipulate it as a proof.
    - pseudonom- 12y ago
      Well, it sounds like what you're looking for is property based testing. You can setup something like QuickCheck to run at compilation.

lmm 12y ago

Only because of inadequate language support (or, in the case of that Ariane 5, deliberately overriding the language support)

TheLoneWolfling 12y ago

Having division by zero being an unchecked exception is a terrible idea, as you say. But that's not what I want. I want a paranoid language. I want a language where potential division by zero is a checked exception. One where "a = b / c" won't even compile if c might be 0. One that won't compile if it can find an example of an input to a function where an assertion fires. I want one where there is no such thing as an unchecked exception. Or rather, one where you can explicitly override checked exceptions to be the equivalent of (read: syntactic sugar for) "except: print(readable exception trace); exit(<code>)" - but you need to explicitly override it to do so. Would it be a pain to write in? Yes. But at the same time there's a lot of software that would be best written in this manner. A language where the language itself forces you to be paranoid.

pseudonom- 12y ago
> One where "a = b / c" won't even compile if c might be 0. Dependently typed languages can provide this.
- TheLoneWolfling 12y ago
  Can you give an example? I have yet to run into a language that doesn't require a proof of correctness, but will just attempt to find a counterexample.
  - lmm 12y ago
    You need to provide a proof, but in e.g. Idris the language gives you the tools to make that proof quite easy.
    - TheLoneWolfling 12y ago
      [Citation needed] Again: I am looking for a language that doesn't require you to provide a proof. I'm looking for a language that is a "logical extension" of what currently is available - that is, I am looking for a language that will attempt to find a counterexample on compilation and will bail if it can.
      - lmm 12y ago
        But non-exhaustively? That exists already - plenty of languages will warn or error if they can tell you're dividing by zero, but don't catch every possible case. Any working program will in some sense be a proof, by Curry-Howard. So I think asking to not have to provide a proof is backwards; what you want is a language that makes it easy to express the program and manipulate it as a proof.
  - pseudonom- 12y ago
    Well, it sounds like what you're looking for is property based testing. You can setup something like QuickCheck to run at compilation.