4 ms·

> And you agreed: I did agree that you can prove some properties about your code. Specifically, you can prove which parts of the code do not perform IO, and in

> And you agreed: I did agree that you can prove some properties about your code. Specifically, you can prove which parts of the code do not perform IO, and in that limited sense "if it compiles, it works" for that example, but that does not hold in general. I did not agree that your code is more likely to be correct in general. The non-IO code may still be wrong (as you said then: it could return the first element of the list instead of the last one) and the IO code may also be wrong. And you have no evidence that any of that code is more likely to be correct. The Haskell compiler can enforce some organization on your code (IO code goes here, non-IO code goes there) but the bugs could still be anywhere. All you have done is to shift the deckchairs on the Titanic! > Most of that bug reduction was made possible by Haskell's purity/immutability. You have no evidence of any actual bug reduction. > You asked for empirical evidence for the inductive claim and I gave it to you. Working deductively from the definition of Haskell is not empirical evidence for the claim that Haskell programs are more likely to be correct.

mightybyte 12y ago
> And you have no evidence that any of that code is more likely to be correct. > You have no evidence of any actual bug reduction. > Working deductively from the definition of Haskell is not empirical evidence for the claim that Haskell programs are more likely to be correct. My deductive reasoning is not the evidence I'm citing here. We counted the total number of ways that a function could go wrong and saw that in pure Haskell code, the number is drastically reduced. We know that the bug types we eliminated actually occur in practice, so under the reasonable assumption that the distribution of bug types is relatively constant, those numbers do provide empirical evidence (observational, not experimental) that Haskell programs are more likely to be correct. Yes, pure code can still be wrong, but it can be wrong in a lot less ways than the impure code that you're stuck with in other languages. That code is still doing useful work that is also bug-prone in other languages. Therefore we can be reasonably confident that it will reduce bugs. If you absolutely insist on experimental evidence, we have that too: https://www.youtube.com/watch?v=BveDrw9CwEg#t=1207 https://www.youtube.com/watch?v=BveDrw9CwEg#t=1207
- infraruby 12y ago
  > My deductive reasoning is not the evidence I'm citing here. You have no evidence, only (invalid) deductions. > We counted the total number of ways that a function could go wrong If you did this it would be deduction. > and saw that in pure Haskell code, the number is drastically reduced. No. Say you have an IO function with two parts, a non-IO part to compute a directory name using some input, and an IO part to remove that directory: rmrf_steamroot some_input = -- some code to compute a directory name using some_input ... -- some code to remove that directory ... Now, the first part does not perform IO, so let's extract that into a non-IO function: compute_directory_name some_input = -- some code to compute a directory name using some_input ... rmrf_steamroot some_input = let directory_name = compute_directory_name some_input -- some code to remove that directory ... How many bugs were removed by doing this? None. It's the same code, just moved about a bit. Sure, the code in the non-IO function "compute_directory_name" does not perform IO (and therefore does not have IO bugs) but that code did not perform IO (and therefore did not have IO bugs) when it was in the original IO function "rmrf_steamroot"! So there is no bug reduction. > those numbers do provide empirical evidence (observational, not experimental) That is not empirical evidence. Perhaps it may help you to read this introduction to the topic: https://en.wikipedia.org/wiki/Empirical_evidence (And where it says "observation or experimentation" it may help if you follow those links.) > If you absolutely insist on experimental evidence, we have that too As you said earlier, they "rewrote a substantial groovy app in Haskell". There are too many confounding variables there.
  - mightybyte 12y ago
    > Say you have an IO function with two parts We're not even arguing about the same thing. I wasn't talking about the rm function, I was talking about the "last" function in my original comment. > If you did this it would be deduction. I did enumerate every possible way that function can go wrong in Haskell. It is precisely n-1 where n is the length of the list (we can ignore the empty list case without loss of generality because it is easy to handle that case statically). In every other language in mainstream use today, the number of ways it could go wrong is infinite. And we actually do see those happen sometimes in practice. The analysis in the above paragraph is the "active acquisition of information from a primary source", i.e. observational evidence for the inductive argument that code written in Haskell is "more likely to be correct". > As you said earlier, they "rewrote a substantial groovy app in Haskell". There are too many confounding variables there. I'm keenly aware of the confounding variables. But the fact is, you're never going to find a significant study that doesn't have a bunch of confounding variables. If that's your criteria for making a decision in this domain, then you won't be accomplishing much. In fact, I doubt we even have strong experimental evidence that C is more productive than assembly language. If you have different people write the different languages, the skill of the people is a confounding variable. If you have the same person write them all, then their knowledge of the languages and their mounting domain experience are confounding variables. So we take whatever evidence we can get. If my bayesian prior was that all languages are equally likely to result in correct programs, then this evidence tips the scale slightly in Haskell's favor. We can't take it to the bank yet, but we've only looked at a couple pieces of evidence. (That's not the only evidence out there, but I'm constraining the discussion to this because of the bandwidth of this communication channel.) Point is, I think we're at the point where savvy forward-looking people should at least take note of Haskell's potential benefits. However much we know now, we will continue to learn more as we observe more and more people using Haskell to build real things.

mightybyte 12y ago

> And you have no evidence that any of that code is more likely to be correct. > You have no evidence of any actual bug reduction. > Working deductively from the definition of Haskell is not empirical evidence for the claim that Haskell programs are more likely to be correct. My deductive reasoning is not the evidence I'm citing here. We counted the total number of ways that a function could go wrong and saw that in pure Haskell code, the number is drastically reduced. We know that the bug types we eliminated actually occur in practice, so under the reasonable assumption that the distribution of bug types is relatively constant, those numbers do provide empirical evidence (observational, not experimental) that Haskell programs are more likely to be correct. Yes, pure code can still be wrong, but it can be wrong in a lot less ways than the impure code that you're stuck with in other languages. That code is still doing useful work that is also bug-prone in other languages. Therefore we can be reasonably confident that it will reduce bugs. If you absolutely insist on experimental evidence, we have that too: https://www.youtube.com/watch?v=BveDrw9CwEg#t=1207 https://www.youtube.com/watch?v=BveDrw9CwEg#t=1207

infraruby 12y ago
> My deductive reasoning is not the evidence I'm citing here. You have no evidence, only (invalid) deductions. > We counted the total number of ways that a function could go wrong If you did this it would be deduction. > and saw that in pure Haskell code, the number is drastically reduced. No. Say you have an IO function with two parts, a non-IO part to compute a directory name using some input, and an IO part to remove that directory: rmrf_steamroot some_input = -- some code to compute a directory name using some_input ... -- some code to remove that directory ... Now, the first part does not perform IO, so let's extract that into a non-IO function: compute_directory_name some_input = -- some code to compute a directory name using some_input ... rmrf_steamroot some_input = let directory_name = compute_directory_name some_input -- some code to remove that directory ... How many bugs were removed by doing this? None. It's the same code, just moved about a bit. Sure, the code in the non-IO function "compute_directory_name" does not perform IO (and therefore does not have IO bugs) but that code did not perform IO (and therefore did not have IO bugs) when it was in the original IO function "rmrf_steamroot"! So there is no bug reduction. > those numbers do provide empirical evidence (observational, not experimental) That is not empirical evidence. Perhaps it may help you to read this introduction to the topic: https://en.wikipedia.org/wiki/Empirical_evidence (And where it says "observation or experimentation" it may help if you follow those links.) > If you absolutely insist on experimental evidence, we have that too As you said earlier, they "rewrote a substantial groovy app in Haskell". There are too many confounding variables there.
- mightybyte 12y ago
  > Say you have an IO function with two parts We're not even arguing about the same thing. I wasn't talking about the rm function, I was talking about the "last" function in my original comment. > If you did this it would be deduction. I did enumerate every possible way that function can go wrong in Haskell. It is precisely n-1 where n is the length of the list (we can ignore the empty list case without loss of generality because it is easy to handle that case statically). In every other language in mainstream use today, the number of ways it could go wrong is infinite. And we actually do see those happen sometimes in practice. The analysis in the above paragraph is the "active acquisition of information from a primary source", i.e. observational evidence for the inductive argument that code written in Haskell is "more likely to be correct". > As you said earlier, they "rewrote a substantial groovy app in Haskell". There are too many confounding variables there. I'm keenly aware of the confounding variables. But the fact is, you're never going to find a significant study that doesn't have a bunch of confounding variables. If that's your criteria for making a decision in this domain, then you won't be accomplishing much. In fact, I doubt we even have strong experimental evidence that C is more productive than assembly language. If you have different people write the different languages, the skill of the people is a confounding variable. If you have the same person write them all, then their knowledge of the languages and their mounting domain experience are confounding variables. So we take whatever evidence we can get. If my bayesian prior was that all languages are equally likely to result in correct programs, then this evidence tips the scale slightly in Haskell's favor. We can't take it to the bank yet, but we've only looked at a couple pieces of evidence. (That's not the only evidence out there, but I'm constraining the discussion to this because of the bandwidth of this communication channel.) Point is, I think we're at the point where savvy forward-looking people should at least take note of Haskell's potential benefits. However much we know now, we will continue to learn more as we observe more and more people using Haskell to build real things.