6 ms·
[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 w
by 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.