3 ms·

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 p

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
- logicchains 8y ago
  I said "Note I mean proven correct, proven to do exactly as specified, not just proven to lack certain classes of bugs.". Model checkers don't prove functional correctness, they just prove the absence of certain kinds of bugs. Sure, if you don't care about correctness model checkers are great, but if you do care about proving a program does exactly as specified then you'll have a much easier time with a functional language.

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

logicchains 8y ago
I said "Note I mean proven correct, proven to do exactly as specified, not just proven to lack certain classes of bugs.". Model checkers don't prove functional correctness, they just prove the absence of certain kinds of bugs. Sure, if you don't care about correctness model checkers are great, but if you do care about proving a program does exactly as specified then you'll have a much easier time with a functional language.