[pka]

> The type system in Java also failed to catch the bug

Java is not a theorem prover, and your comment was about theorem provers.

> you wouldn't end up with an error in a specification

Again, completely orthogonal to your argument. If you have an error in specification tests won't help you because you'll test the wrong thing.

> The thing to realize is that theorem proving is not a business goal in most cases. What you care about is being able to deliver software that works

Again, your comment was about "saying things are correct in the semantic sense". You're saying now "I don't care about correctness in the semantic sense, I care about delivering software that "works" (whatever this means; clearly it doesn't mean software without bugs) in a reasonable amount of time" and that's fine. I do too, but again, nothing to do with your original argument.

[yogthos]

>Java is not a theorem prover, and your comment was about theorem provers.

No, my comment was about formal methods in general. Every type system is a form of a machine assisted proof in practice. It's just that most type systems don't allow you to prove interesting things about your code.

The main problem is that of basic cost/benefit analysis. If it takes significantly more effort to write a full formal proof, and you end up sometimes catching minor errors, the effort is not justified in most scenarios.

>Again, completely orthogonal to your argument. If you have an error in specification tests won't help you because you'll test the wrong thing.

This is completely central to my argument. I'm saying that encoding a meaningful specification using a type system is a lot more difficult than doing that using runtime contracts, or even simply reasoning about the code unassisted.

I can read through the 5 lines of Python code implementing insertion code, and be reasonably sure that it's correct. I would have a much harder time verifying that 300 lines of Idris are specifying what was intended.

> You're saying now "I don't care about correctness in the semantic sense, I care about delivering software that "works" (whatever this means; clearly it doesn't mean software without bugs) in a reasonable amount of time" and that's fine. I do too, but again, nothing to do with your original argument.

I'm saying that you have diminishing returns. What you want to show is semantic correctness, and type systems are a poor tool for doing that. So, while you can use a type system to do that in principle, the effort is not justified vast majority of the time.

[pka]

> I can read through the 5 lines of Python code implementing insertion code, and be reasonably sure that it's correct.

Binary search is possibly one of the simplest and most basic CS algorithms, and yet, it took people who were "reasonably sure" 10 years to find that bug.

> I would have a much harder time verifying that 300 lines of Idris are specifying what was intended.

Then don't use Idris?

> I'm saying that you have diminishing returns.

I agree. However, that was not your argument. Your argument was that tests subsume proofs, and that's obviously wrong.

Also, types vs tests is a false dichotomy. Personally, I find a strongly typed language + QuickCheck to be the most practical way of developing complex software. YMMV, and that's fine.

[yogthos]

>Binary search is possibly one of the simplest and most basic CS algorithms, and yet, it took people who were "reasonably sure" 10 years to find that bug.

Again, saying there is a bug is not interesting. The question is how much this bug costs you, and how much time you're willing to invest in order to guarantee that you won't make that type of a bug.

>Then don't use Idris?

I think you entirely missed the point I was making here.

>I agree. However, that was not your argument. Your argument was that tests subsume proofs, and that's obviously wrong.

My point is that tests and runtime contracts provide sufficient guarantees in practice. Nowhere have I argued that they provide the same guarantees as proofs. The argument is that the cost of the proofs is much higher, and the proofs themselves can be harder to reason about making it harder to tell they're proving the right thing.

Consider the case of Fermat's last theorem as an example. It's pretty easy to state: a^n + b^n = c^n, and it's easy to test that this is the case for a given set of inputs that you might care about. However proving that to be the case for all possible inputs is a monumental task, and there are only a handful of people in the world who would even be able to follow the proof.

>Also, types vs tests is a false dichotomy. Personally, I find a strongly typed language + QuickCheck to be the most practical way of developing complex software. YMMV, and that's fine.

Again, that is not a dichotomy I was suggesting. My point was that I think runtime contracts are a more effective way to provide a semantic specification than a static type system. I also said that static typing restricts how you're able to express yourself, leading to code that's optimized for the benefit of the type checker as opposed to that of the human reader. I'm not sure how you got types vs tests from that.

[pka]

> Reading and understanding the Idris proof is actually more work than understanding the untyped Python version, therefore it's actually harder to say whether it's correct or not in a semantic sense.

That was your original, nonsensical, point (emphasis mine).

> My point is that tests and runtime contracts provide sufficient guarantees in practice.

That's your revised point (which I don't care much about discussing), after moving the goalposts sufficiently.