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