Hacker News Reader

> One where "a = b / c" won't even compile if c might be 0.

Dependently typed languages can provide this.

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.

You need to provide a proof, but in e.g. Idris the language gives you the tools to make that proof quite easy.

[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.

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.

Well, it sounds like what you're looking for is property based testing. You can setup something like QuickCheck to run at compilation.

Reply on news.ycombinator.com