4 ms·

1. Here: https://news.ycombinator.com/item?id=19586915 https://news.ycombinator.com/item?id=19586915 > Explaining why it is unlikely (from a theory perspective

1. Here: https://news.ycombinator.com/item?id=19586915 https://news.ycombinator.com/item?id=19586915 > Explaining why it is unlikely (from a theory perspective) that languages like Haskell have a significant effect on correctness is easier [2] > It's relatively easy to classify which program properties can be assisted by the language and which cannot. Those that can (e.g. memory safety and type safety) are called inductive (or compositional). They can be helpful, but the vast majority of correctness properties aren't inductive. Inductive/compositional means that the property is preserved by all primitive operations in the language. 2. Because homeopathy's claims and method of action can be dismissed a priori, due to the fact that they don't follow the laws of nature or the chemical principles of solvation. Further, your are conflating the question " could (typed) FP be use for correctness" with " should (typed) FP be use for correctness", and while the answer to the first one is trivially "yes", you appear to be chasing the answer you want ("no") to the second question. This puts your approach closer to that of the homeopaths.

pron 8y ago
I mentioned type safety in passing, but I wasn't talking about the effect of types on correctness in this discussion. That's a more nuanced one. > your are conflating the question " could (typed) FP be use for correctness" with " should (typed) FP be use for correctness", and while the answer to the first one is trivially "yes", you appear to be chasing the answer you want ("no") to the second question. I am not conflating anything, and I certainly didn't say which programming paradigm people should or shouldn't use. I did say that if people care about correctness, they should look elsewhere than to change their preferred paradigm to or from FP, and focus on techniques that seem to have an actual effect on correctness (BTW, switching languages -- among several reasonable choices -- is often costly, and language in general is one of the choices with the least drastic effect on most important software metrics, except maybe when it comes to performance, where most of the time what matters is the runtime, and not so much the programming paradigm). BTW, while I won't get into the discussion about types (which, again, is complicated, as there are different kind of types and usage of types, each with very different cost/benefit), the largest effect types -- and language choice in general -- have on correctness was found in a study I linked in another comment to be of 15% (in bug reduction), when comparing TypeScript and JavaScript. In contrast, several studies and case studies have found code reviews to have an average effect of ~60%. So the largest effect language choice was ever found to have in a single study is 4x smaller than the effect of techniques that are far cheaper than a language change (well, maybe not in the case of TypeScript/JavaScript). Really, language is one of the costliest and least impactful factors on correctness (except maybe when the language is unsafe). In summary, no connection between FP and correctness has been established, period (and what little evidence we have seems to suggest there is none). People should use whatever paradigm/language they like; the chosen paradigm doesn't seem to have a large positive or a negative effect on correctness. People shouldn't make empirical claims that are unsubstantiated. > Because homeopathy's claims and method of action can be dismissed a priori, due to the fact that they don't follow the laws of nature or the chemical principles of solvation. I wasn't trying to say that people who believe FP has an effect on correctness are exactly the same as those who believe in the effectiveness of homeopathy. I only said that the fact that some people make the claim enthusiastically in blog posts should not be taken as corroboration to its validity, just as the number of enthusiastic posts about homeopathy is not evidence in its favor. People often enthusiastically believe things that aren't true because personal experience can be misleading. But anyway, the claim that FP improves correctness similarly does not follow any law of software correctness. If either homeopathy or FP were to have an effect, it would have to be through some as-of-yet undiscovered process. As any program could be mechanically translated between pure-FP and imperative, there is simply no CS theory to explain why FP would have an effect on correctness (as opposed to, say, using a model checker), and there is no such programming-process theory, either (as opposed to, say, code reviews).
- cannabis_sam 8y ago
  >I mentioned type safety in passing Thank you, that's what I meant. > The claim that FP improves correctness similarly does not follow any law of software correctness. If either homeopathy or FP were to have an effect, it would have to be through some as-of-yet undiscovered process. Again you are conflating could and should. Let's simplify: Homeopathy CANNOT be used, since the concept fundamentally don't work and hence SHOULD not be used. FP for correctness CAN be used, since we do have examples of functional languages that can be used with formal verification tools, type-based or otherwise. Whether it SHOULD be used, does not follow from whether it CAN/CANNOT be used. That's a question for the sociology of software engineering, and like you say, that's complex. >People should use whatever paradigm/language they like I agree, which is why I dislike when people try to associate certain preferences with pseudoscience.

pron 8y ago

I mentioned type safety in passing, but I wasn't talking about the effect of types on correctness in this discussion. That's a more nuanced one. > your are conflating the question " could (typed) FP be use for correctness" with " should (typed) FP be use for correctness", and while the answer to the first one is trivially "yes", you appear to be chasing the answer you want ("no") to the second question. I am not conflating anything, and I certainly didn't say which programming paradigm people should or shouldn't use. I did say that if people care about correctness, they should look elsewhere than to change their preferred paradigm to or from FP, and focus on techniques that seem to have an actual effect on correctness (BTW, switching languages -- among several reasonable choices -- is often costly, and language in general is one of the choices with the least drastic effect on most important software metrics, except maybe when it comes to performance, where most of the time what matters is the runtime, and not so much the programming paradigm). BTW, while I won't get into the discussion about types (which, again, is complicated, as there are different kind of types and usage of types, each with very different cost/benefit), the largest effect types -- and language choice in general -- have on correctness was found in a study I linked in another comment to be of 15% (in bug reduction), when comparing TypeScript and JavaScript. In contrast, several studies and case studies have found code reviews to have an average effect of ~60%. So the largest effect language choice was ever found to have in a single study is 4x smaller than the effect of techniques that are far cheaper than a language change (well, maybe not in the case of TypeScript/JavaScript). Really, language is one of the costliest and least impactful factors on correctness (except maybe when the language is unsafe). In summary, no connection between FP and correctness has been established, period (and what little evidence we have seems to suggest there is none). People should use whatever paradigm/language they like; the chosen paradigm doesn't seem to have a large positive or a negative effect on correctness. People shouldn't make empirical claims that are unsubstantiated. > Because homeopathy's claims and method of action can be dismissed a priori, due to the fact that they don't follow the laws of nature or the chemical principles of solvation. I wasn't trying to say that people who believe FP has an effect on correctness are exactly the same as those who believe in the effectiveness of homeopathy. I only said that the fact that some people make the claim enthusiastically in blog posts should not be taken as corroboration to its validity, just as the number of enthusiastic posts about homeopathy is not evidence in its favor. People often enthusiastically believe things that aren't true because personal experience can be misleading. But anyway, the claim that FP improves correctness similarly does not follow any law of software correctness. If either homeopathy or FP were to have an effect, it would have to be through some as-of-yet undiscovered process. As any program could be mechanically translated between pure-FP and imperative, there is simply no CS theory to explain why FP would have an effect on correctness (as opposed to, say, using a model checker), and there is no such programming-process theory, either (as opposed to, say, code reviews).

cannabis_sam 8y ago
>I mentioned type safety in passing Thank you, that's what I meant. > The claim that FP improves correctness similarly does not follow any law of software correctness. If either homeopathy or FP were to have an effect, it would have to be through some as-of-yet undiscovered process. Again you are conflating could and should. Let's simplify: Homeopathy CANNOT be used, since the concept fundamentally don't work and hence SHOULD not be used. FP for correctness CAN be used, since we do have examples of functional languages that can be used with formal verification tools, type-based or otherwise. Whether it SHOULD be used, does not follow from whether it CAN/CANNOT be used. That's a question for the sociology of software engineering, and like you say, that's complex. >People should use whatever paradigm/language they like I agree, which is why I dislike when people try to associate certain preferences with pseudoscience.