4 ms·

As someone who practices and encourages others to employ formal methods in software development, I'm disappointed to read a post that claims FP has some signifi

by pron 8y ago

As someone who practices and encourages others to employ formal methods in software development, I'm disappointed to read a post that claims FP has some significant effect on correctness. This has not been established, and does not at all appear to be the case. There are many aspects, including techniques and tools, that can positively affect program correctness. The choice of a programming language or even a paradigm is not high on the list if it is on it at all. Not only does the little data we have not substantiate the hypothesis that FP has a significant positive effect on correctness, there are even significantly fewer anecdotal reports supporting that hypothesis than other, apparently more effective techniques. In short, any connection between FP and correctness is, at this point in time, nothing more than wishful thinking, and the efforts of those who really care about correctness are better spent elsewhere (i.e. not on picking a new language).

sevensor 8y ago
There are certainly a lot of people who feel that way, though. Especially when the language has an expressive type system. Would you say these languages merely swap one kind of error for another?
- pron 8y ago
  There are certainly quite a lot of people who feel homeopathy is effective. In both cases, that feeling is a result of a complex process [1]. Explaining why it is unlikely (from a theory perspective) that languages like Haskell have a significant effect on correctness is easier [2], but it, too, requires much more space. What is simple to show is that organizations that develop in, say, Haskell do not produce more correct software more cheaply (or some combination of the two) than those that use other languages. [1]: For example, in this case, what you call "a lot" may just be the effect of some sort of enthusiasm that results in publications rather than an actual great number of people. Also, the feeling can be the result of programmers facing an unfamiliar language that is challenging them, hence they are required to focus and think more, and that gives them a feeling that they're writing something that's more correct. That the languages catches early some errors may also strengthen this feeling. They're also likely writing smaller programs. I've programmed in many languages, and one of the languages where I get it right most quickly is assembly, probably because I write smaller things, and because I need to focus much more. [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.
  - sevensor 8y ago
    Interesting! Thanks for a detailed reply. Since you bring up the cost of software, do you believe that using formal methods helps reduce costs?
    - pron 8y ago
      Formal methods encompass a very wide range of techniques that vary wildly in cost. When the appropriate technique is applied to the appropriate problem, then it can certainly reduce costs, even significantly. But like I wrote in another comment, most of the cost of building software is determined by what we build, not how. Tools and techniques, even those that are effective, can only help so much.
  - marcosdumay 8y ago
    There is a large amount of evidence that shows that homeopathy isn't effective. As far as evidence goes, there is more evidence pointing that FP leads to correctness than otherwise, although none of it is conclusive.
    - pron 8y ago
      > There is a large amount of evidence that shows that homeopathy isn't effective. That's not quite how evidence for the existence of effects works. Evidence for lack of an effect is the attempt, and subsequent failure, to find it. Few studies have been able to substantiate the hypothesis that homeopathy is very effective, just like the case for FP. It's just that there have been far fewer studies overall testing the second hypothesis than the first. So while we can be more confident that, indeed, homeopathy isn't effective than in the case of FP, there is still no weight to the claim that FP is effective when it comes to correctness. > there is more evidence pointing that FP leads to correctness than otherwise There isn't. It's perfectly OK that people write about how much they like FP or OOP because the paradigm fits well with how they think, they like its aesthetics, or any similar reasons. It's not OK to try and justify the preference by making up completely unsupported empirical claims. And by the way, even when there is no evidence one way or the other, you still cannot claim there is an effect.
- mpweiher 8y ago
  > who feel that way You hit the nail on the head: The Safyness of Static Typing https://blog.metaobject.com/2014/06/the-safyness-of-static-typing.html https://blog.metaobject.com/2014/06/the-safyness-of-static-t... (This is obviously for static typing, not FP, but the mechanism appears largely the same and the overlap is substantial)
logicchains 8y ago
Can you point to a project as complex as CompCert (formally verified C compiler) that's been written and proven correct in an imperative language? Note I mean proven correct, proven to do exactly as specified, not just proven to lack certain classes of bugs.
- pron 8y ago
  Absolutely, but first, CompCert is not really a good example for verification. It is a very small program (roughly equivalent to 10KLOC of C; i.e. 1/5th the size of jQuery), it has taken years of effort by world experts, and they had to cut quite a few corners so your classification of what exactly has been proven is also exaggerated (watch talks by Xavier Leroy [1]). It is more a heroic story of people who climbed the Everest naked than some generalizable technique. But heroic and impressive it was. Now, CompCert was verified using deductive proofs. In industry, this is an approach that's hardly used (in part, CompCert was done to show that it could be used at all, at least in principle). Verification in industry is normally done using model checkers, that are fully automated. There are tradeoffs between deductive proofs and model checkers (and sometimes deductive proofs are used to close some holes left by model checkers, or tie together some modules verified by model chekcers [2]), but they scale better. Model checkers used in industry include Spin[3], nuSMV[4] and others. So model checkers check software that's larger than CompCert every day, but they don't get papers written about them, because their use is more mundane than heroic. They are also used for imperative languages, because formal verification of functional programs is behind (here is Simon Peyton Jones saying that [5]). Model checking functional languages is hard, because higher-order functions are hard to verify. Instead, there are model checkers for C, Java, hardware definition languages and tool-specific languages. So, this mentions a 1MLOC Java application by Fujitsu that's been model checked[6] with NASA's Java model checker (that's 10x bigger than CompCert), and here's a report about model checking a many small C programs[7]. Again, software verification of imperative languages is almost mundane; what you read about are exceptional things. Also, people who are interested in programming languages are normally introduced to formal methods through its small intersection with programming language theory, and that intersection includes uses of proof assistants and dependent types. Because functional languages are liked by language theorists (for many reasons I won't go into), then that's what you see. But that is a very small part of formal methods research. Most of it is research into model checking and sound static analysis, and most of that work is done in imperative languages. Not because they're easier to verify (both functional and imperative are just as hard, but pose different challenges), but because they want to check programs in languages many people use, and language doesn't make much of a difference. Finally, I should add that even though language doesn't have a huge impact (there can be some exceptions; e.g. unsafe languages such as C do add some challenges), there are languages that are more natural for verification; they are not functional or classically imperative, though, as those two are both mediocre. Rather, those languages are synchronous languages (usually imperative, but not like what you're used to). Normally, those languages are used in hardware and real-time software (Esterel[8], SCADE[9], but they are now starting to make their way into the mainstream with Céu[10], "behavioral programming" in JavaScript [11], and, perhaps most famously, with Eve [12] (RIP). To see why these synchronous (but imperative) languages are a good fit for verification, take a look at how easy it is to specify a correctness property in Eve: [13]. Finally, my own favorite specification and verification language is TLA+ [14], which is neither functional nor imperative (but it is synchronous; then again, it's not a programming language), has been used to verify very large programs at Amazon and elsewhere [15]. To get back to where I started, CompCert (and seL4) are not really examples of anything. They were both huge, heroic efforts (that didn't quite prove as much as you think they did) by academics in the lab on quite tiny programs. While these efforts are important for some niches, you can't generalize, just as you can't generalize from the design of particle accelerators used to turn some lead atoms into gold atoms to learn about how best to design metalworking tools. Full, end-to-end verification, is something that we simply aren't yet capable of doing in any generalizable or scalable way, regardless of language. Real-world verification efforts are quite different, and are done with imperative languages both because that's what people use and the language doesn't have a big impact, and becuase there are still issues with model checking functional programming languages. [1]: http://video.upmc.fr/differe.php?collec=S_C_colloquium_lip6_2012&video=19 http://video.upmc.fr/differe.php?collec=S_C_colloquium_lip6_... [2]: http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.html http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.h... [3]: http://spinroot.com/spin/whatispin.html http://spinroot.com/spin/whatispin.html [4]: http://nusmv.fbk.eu/ http://nusmv.fbk.eu/ [5]: http://events.inf.ed.ac.uk/Milner2012/Monday_Panel-html5-mp4.html http://events.inf.ed.ac.uk/Milner2012/Monday_Panel-html5-mp4... [6]: http://javapathfinder.sourceforge.net/events/JPF-workshop-050108/SymbolicJPF08.pdf http://javapathfinder.sourceforge.net/events/JPF-workshop-05... [7]: http://www.csl.sri.com/users/ddean/papers/ndss04.pdf http://www.csl.sri.com/users/ddean/papers/ndss04.pdf [8]: https://en.wikipedia.org/wiki/Esterel https://en.wikipedia.org/wiki/Esterel [9]: http://www.esterel-technologies.com/products/scade-suite/ http://www.esterel-technologies.com/products/scade-suite/ [10]: http://ceu-lang.org/ http://ceu-lang.org/ [11]: https://youtu.be/PW8VdWA0UcA https://youtu.be/PW8VdWA0UcA , https://vimeo.com/298554103 https://vimeo.com/298554103 [12]: http://witheve.com/ http://witheve.com/ [13]: http://witheve.com/#correct http://witheve.com/#correct [14]: https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html [15]: https://lamport.azurewebsites.net/tla/industrial-use.html https://lamport.azurewebsites.net/tla/industrial-use.html

by pron 8y ago

sevensor 8y ago

There are certainly a lot of people who feel that way, though. Especially when the language has an expressive type system. Would you say these languages merely swap one kind of error for another?

pron 8y ago
There are certainly quite a lot of people who feel homeopathy is effective. In both cases, that feeling is a result of a complex process [1]. Explaining why it is unlikely (from a theory perspective) that languages like Haskell have a significant effect on correctness is easier [2], but it, too, requires much more space. What is simple to show is that organizations that develop in, say, Haskell do not produce more correct software more cheaply (or some combination of the two) than those that use other languages. [1]: For example, in this case, what you call "a lot" may just be the effect of some sort of enthusiasm that results in publications rather than an actual great number of people. Also, the feeling can be the result of programmers facing an unfamiliar language that is challenging them, hence they are required to focus and think more, and that gives them a feeling that they're writing something that's more correct. That the languages catches early some errors may also strengthen this feeling. They're also likely writing smaller programs. I've programmed in many languages, and one of the languages where I get it right most quickly is assembly, probably because I write smaller things, and because I need to focus much more. [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.
- sevensor 8y ago
  Interesting! Thanks for a detailed reply. Since you bring up the cost of software, do you believe that using formal methods helps reduce costs?
  - pron 8y ago
    Formal methods encompass a very wide range of techniques that vary wildly in cost. When the appropriate technique is applied to the appropriate problem, then it can certainly reduce costs, even significantly. But like I wrote in another comment, most of the cost of building software is determined by what we build, not how. Tools and techniques, even those that are effective, can only help so much.
- marcosdumay 8y ago
  There is a large amount of evidence that shows that homeopathy isn't effective. As far as evidence goes, there is more evidence pointing that FP leads to correctness than otherwise, although none of it is conclusive.
  - pron 8y ago
    > There is a large amount of evidence that shows that homeopathy isn't effective. That's not quite how evidence for the existence of effects works. Evidence for lack of an effect is the attempt, and subsequent failure, to find it. Few studies have been able to substantiate the hypothesis that homeopathy is very effective, just like the case for FP. It's just that there have been far fewer studies overall testing the second hypothesis than the first. So while we can be more confident that, indeed, homeopathy isn't effective than in the case of FP, there is still no weight to the claim that FP is effective when it comes to correctness. > there is more evidence pointing that FP leads to correctness than otherwise There isn't. It's perfectly OK that people write about how much they like FP or OOP because the paradigm fits well with how they think, they like its aesthetics, or any similar reasons. It's not OK to try and justify the preference by making up completely unsupported empirical claims. And by the way, even when there is no evidence one way or the other, you still cannot claim there is an effect.
mpweiher 8y ago
> who feel that way You hit the nail on the head: The Safyness of Static Typing https://blog.metaobject.com/2014/06/the-safyness-of-static-typing.html https://blog.metaobject.com/2014/06/the-safyness-of-static-t... (This is obviously for static typing, not FP, but the mechanism appears largely the same and the overlap is substantial)

logicchains 8y ago

Can you point to a project as complex as CompCert (formally verified C compiler) that's been written and proven correct in an imperative language? Note I mean proven correct, proven to do exactly as specified, not just proven to lack certain classes of bugs.

pron 8y ago
Absolutely, but first, CompCert is not really a good example for verification. It is a very small program (roughly equivalent to 10KLOC of C; i.e. 1/5th the size of jQuery), it has taken years of effort by world experts, and they had to cut quite a few corners so your classification of what exactly has been proven is also exaggerated (watch talks by Xavier Leroy [1]). It is more a heroic story of people who climbed the Everest naked than some generalizable technique. But heroic and impressive it was. Now, CompCert was verified using deductive proofs. In industry, this is an approach that's hardly used (in part, CompCert was done to show that it could be used at all, at least in principle). Verification in industry is normally done using model checkers, that are fully automated. There are tradeoffs between deductive proofs and model checkers (and sometimes deductive proofs are used to close some holes left by model checkers, or tie together some modules verified by model chekcers [2]), but they scale better. Model checkers used in industry include Spin[3], nuSMV[4] and others. So model checkers check software that's larger than CompCert every day, but they don't get papers written about them, because their use is more mundane than heroic. They are also used for imperative languages, because formal verification of functional programs is behind (here is Simon Peyton Jones saying that [5]). Model checking functional languages is hard, because higher-order functions are hard to verify. Instead, there are model checkers for C, Java, hardware definition languages and tool-specific languages. So, this mentions a 1MLOC Java application by Fujitsu that's been model checked[6] with NASA's Java model checker (that's 10x bigger than CompCert), and here's a report about model checking a many small C programs[7]. Again, software verification of imperative languages is almost mundane; what you read about are exceptional things. Also, people who are interested in programming languages are normally introduced to formal methods through its small intersection with programming language theory, and that intersection includes uses of proof assistants and dependent types. Because functional languages are liked by language theorists (for many reasons I won't go into), then that's what you see. But that is a very small part of formal methods research. Most of it is research into model checking and sound static analysis, and most of that work is done in imperative languages. Not because they're easier to verify (both functional and imperative are just as hard, but pose different challenges), but because they want to check programs in languages many people use, and language doesn't make much of a difference. Finally, I should add that even though language doesn't have a huge impact (there can be some exceptions; e.g. unsafe languages such as C do add some challenges), there are languages that are more natural for verification; they are not functional or classically imperative, though, as those two are both mediocre. Rather, those languages are synchronous languages (usually imperative, but not like what you're used to). Normally, those languages are used in hardware and real-time software (Esterel[8], SCADE[9], but they are now starting to make their way into the mainstream with Céu[10], "behavioral programming" in JavaScript [11], and, perhaps most famously, with Eve [12] (RIP). To see why these synchronous (but imperative) languages are a good fit for verification, take a look at how easy it is to specify a correctness property in Eve: [13]. Finally, my own favorite specification and verification language is TLA+ [14], which is neither functional nor imperative (but it is synchronous; then again, it's not a programming language), has been used to verify very large programs at Amazon and elsewhere [15]. To get back to where I started, CompCert (and seL4) are not really examples of anything. They were both huge, heroic efforts (that didn't quite prove as much as you think they did) by academics in the lab on quite tiny programs. While these efforts are important for some niches, you can't generalize, just as you can't generalize from the design of particle accelerators used to turn some lead atoms into gold atoms to learn about how best to design metalworking tools. Full, end-to-end verification, is something that we simply aren't yet capable of doing in any generalizable or scalable way, regardless of language. Real-world verification efforts are quite different, and are done with imperative languages both because that's what people use and the language doesn't have a big impact, and becuase there are still issues with model checking functional programming languages. [1]: http://video.upmc.fr/differe.php?collec=S_C_colloquium_lip6_2012&video=19 http://video.upmc.fr/differe.php?collec=S_C_colloquium_lip6_... [2]: http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.html http://events.inf.ed.ac.uk/Milner2012/J_Harrison-html5-mp4.h... [3]: http://spinroot.com/spin/whatispin.html http://spinroot.com/spin/whatispin.html [4]: http://nusmv.fbk.eu/ http://nusmv.fbk.eu/ [5]: http://events.inf.ed.ac.uk/Milner2012/Monday_Panel-html5-mp4.html http://events.inf.ed.ac.uk/Milner2012/Monday_Panel-html5-mp4... [6]: http://javapathfinder.sourceforge.net/events/JPF-workshop-050108/SymbolicJPF08.pdf http://javapathfinder.sourceforge.net/events/JPF-workshop-05... [7]: http://www.csl.sri.com/users/ddean/papers/ndss04.pdf http://www.csl.sri.com/users/ddean/papers/ndss04.pdf [8]: https://en.wikipedia.org/wiki/Esterel https://en.wikipedia.org/wiki/Esterel [9]: http://www.esterel-technologies.com/products/scade-suite/ http://www.esterel-technologies.com/products/scade-suite/ [10]: http://ceu-lang.org/ http://ceu-lang.org/ [11]: https://youtu.be/PW8VdWA0UcA https://youtu.be/PW8VdWA0UcA , https://vimeo.com/298554103 https://vimeo.com/298554103 [12]: http://witheve.com/ http://witheve.com/ [13]: http://witheve.com/#correct http://witheve.com/#correct [14]: https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html [15]: https://lamport.azurewebsites.net/tla/industrial-use.html https://lamport.azurewebsites.net/tla/industrial-use.html