4 ms·
> One where "a = b / c" won't even compile if c might be 0. Dependently typed languages can provide this.
by 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 agoCan 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 agoYou 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 agoBut 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 agoWell, it sounds like what you're looking for is property based testing. You can setup something like QuickCheck to run at compilation.