6 ms·

Of course most of the money has been funding tools for imperative languages as that is the status quo. But this does not prove that there is little overlap with

by willtim 10y ago

Of course most of the money has been funding tools for imperative languages as that is the status quo. But this does not prove that there is little overlap with FP. Research FP languages like Coq have enabled INRIA to build a fully verified C compiler (Compcert), can your tools accomplish this? As far as Europe is concerned, FP does appear to be the future of formal verification.

pron 10y ago
> Research FP languages like Coq have enabled INRIA to build a fully verified C compiler (Compcert), can your tools accomplish this? First of all, end-to-end verification is something very unique. CompCert is a great accomplishment, but it is only a medium-sized program, it required a world-expert to write, and even then it tool a lot of effort and still he skimped on the termination proofs. Imperative tools, OTOH, are used every day by thousands of engineers to write verified software of various kinds (e.g., [1]). So the answer to your question is: except for end-to-end verification, which is extremely costly with any approach, they can do better. In fact, as promising as FP approaches may be, they are still very much in the lab with nearly negligible industry use (and in the one or two cases Coq has been used in the industry, it was always done jointly with academics). Also, I'm a bit puzzled because you specifically mentioned OCaml, which is an imperative functional language. In fact, while the difference between programming language in terms of general amenability to formal methods is not great, there are certainly large differences in amenability to model checking. This is why a language like SCADE (based on Esterel and the FRP-ish Lustre) is a fairly widely used tool in aviation software. If anything, a synchronous language like Esterel or the modern Céu[2] are a better choice if you want your verification to be as automatic as possible and run in a resource-constrained environment (that's killing two birds with one stone). > As far as Europe is concerned, FP does appear to be the future of formal verification. Even if you look at INRIA, the most European of institutions and the birthplace of Coq, you'll see that they dedicate significant verification research to other approaches[3]. At Max Planck, FP is a clear minority[4]. And if you look at the academic community at large without artificially restricting it to Europe (which certainly has a linguistic bias), you'll see that the verification community is certainly not betting on FP (although they are certainly exploring it). Don't get me wrong: FP and linguistic approaches is certainly one avenue among several showing promise in verification. But it is downright false to say that this approach is recognized as "the future of verification". [1]: https://verificationinstitute.org/wp-content/uploads/sites/28/2016/05/White-Slides.pdf https://verificationinstitute.org/wp-content/uploads/sites/2... [2]: http://www.ceu-lang.org/ http://www.ceu-lang.org/ [3]: http://www.inria.fr/en/teams/veridis http://www.inria.fr/en/teams/veridis [4]: http://plv.mpi-sws.org/ http://plv.mpi-sws.org/
- willtim 10y ago
  I mentioned Lexifi, a contract language, which is based on OCaml and is not imperative. I restricted my argument to Europe as we appear to be less commercially influenced (e.g. MIT teach freshmen Python, Oxford teach Haskell). Predicting the future is always subjective. I offered only my opinion.
  - pron 10y ago
    > I mentioned Lexifi, ... which is based on OCaml and is not imperative. Oh, sorry. > we appear to be less commercially influenced I don't think this has anything to do with commercial influence -- just academic tradition and maybe even philosophical influences: I think you'll get different answers to the question, "does an algorithm or a computation exist outside its description in a language, and if so, in what way?" This may be tied to actual philosophies, Derrida in France vs. Kripke in the US[1] (to prove the connection, a "Kripke structure" is a very common mathematical structure denoting an "abstract" computation, which is used commonly in non-language-based verification). I've been told that the study of program semantics tries to reconcile the two. As to Haskell vs. Python, first, MIT used to teach Scheme; they have explained their reasons for switching to Python. Second, this difference is more indicative of the competition between "theory A" and "theory B". Theory A studies algorithms and complexity (and Haskell is not the best first pedagogical choice for that), while theory B studies logic and semantics (and language). Theory B is relatively small, but it does have a stronger presence in Europe. Although, even within theory B there seem to be those who prefer linguistic approaches (semantics) and those who prefer conceptual approaches (Kripke structures, abstract machines). [1]: Not that Britain is too fond of French philosophy, but the Brits had Robin Milner, who is as close to a CS deconstructionist as you could find.
    - willtim 10y ago
      It's worth pointing out that most of the formal methods you have linked to involve contracts or specifications as separate stratified layers written in various logics. No Turing Machines involved. This is essentially functional programming as far as I'm concerned. The advantage of the dependant-type approaches like Coq and Agda, is that the language of proof and implementation is now one of the same, but I was not necessarily advocating their use as you seem to have assumed. Even without dependent types, a total functional program can serve as both an executable specification and a logic with which one can derive proofs from (e.g. via an SMT solver). This is what I meant when I said functional programming is more amenable to formal methods. So any tool that uses dataflow analysis to convert imperative programs into functional ones, or requires me to write functional programs to describe what the imperative program should be doing, doesn't provide a counter argument in my mind. Finally, in my very first comment, I provided a link to a startup who are planning on using FP and SMT solvers for formal verification of blockchain contracts, so watch this space...

by willtim 10y ago

pron 10y ago

> Research FP languages like Coq have enabled INRIA to build a fully verified C compiler (Compcert), can your tools accomplish this? First of all, end-to-end verification is something very unique. CompCert is a great accomplishment, but it is only a medium-sized program, it required a world-expert to write, and even then it tool a lot of effort and still he skimped on the termination proofs. Imperative tools, OTOH, are used every day by thousands of engineers to write verified software of various kinds (e.g., [1]). So the answer to your question is: except for end-to-end verification, which is extremely costly with any approach, they can do better. In fact, as promising as FP approaches may be, they are still very much in the lab with nearly negligible industry use (and in the one or two cases Coq has been used in the industry, it was always done jointly with academics). Also, I'm a bit puzzled because you specifically mentioned OCaml, which is an imperative functional language. In fact, while the difference between programming language in terms of general amenability to formal methods is not great, there are certainly large differences in amenability to model checking. This is why a language like SCADE (based on Esterel and the FRP-ish Lustre) is a fairly widely used tool in aviation software. If anything, a synchronous language like Esterel or the modern Céu[2] are a better choice if you want your verification to be as automatic as possible and run in a resource-constrained environment (that's killing two birds with one stone). > As far as Europe is concerned, FP does appear to be the future of formal verification. Even if you look at INRIA, the most European of institutions and the birthplace of Coq, you'll see that they dedicate significant verification research to other approaches[3]. At Max Planck, FP is a clear minority[4]. And if you look at the academic community at large without artificially restricting it to Europe (which certainly has a linguistic bias), you'll see that the verification community is certainly not betting on FP (although they are certainly exploring it). Don't get me wrong: FP and linguistic approaches is certainly one avenue among several showing promise in verification. But it is downright false to say that this approach is recognized as "the future of verification". [1]: https://verificationinstitute.org/wp-content/uploads/sites/28/2016/05/White-Slides.pdf https://verificationinstitute.org/wp-content/uploads/sites/2... [2]: http://www.ceu-lang.org/ http://www.ceu-lang.org/ [3]: http://www.inria.fr/en/teams/veridis http://www.inria.fr/en/teams/veridis [4]: http://plv.mpi-sws.org/ http://plv.mpi-sws.org/

willtim 10y ago
I mentioned Lexifi, a contract language, which is based on OCaml and is not imperative. I restricted my argument to Europe as we appear to be less commercially influenced (e.g. MIT teach freshmen Python, Oxford teach Haskell). Predicting the future is always subjective. I offered only my opinion.
- pron 10y ago
  > I mentioned Lexifi, ... which is based on OCaml and is not imperative. Oh, sorry. > we appear to be less commercially influenced I don't think this has anything to do with commercial influence -- just academic tradition and maybe even philosophical influences: I think you'll get different answers to the question, "does an algorithm or a computation exist outside its description in a language, and if so, in what way?" This may be tied to actual philosophies, Derrida in France vs. Kripke in the US[1] (to prove the connection, a "Kripke structure" is a very common mathematical structure denoting an "abstract" computation, which is used commonly in non-language-based verification). I've been told that the study of program semantics tries to reconcile the two. As to Haskell vs. Python, first, MIT used to teach Scheme; they have explained their reasons for switching to Python. Second, this difference is more indicative of the competition between "theory A" and "theory B". Theory A studies algorithms and complexity (and Haskell is not the best first pedagogical choice for that), while theory B studies logic and semantics (and language). Theory B is relatively small, but it does have a stronger presence in Europe. Although, even within theory B there seem to be those who prefer linguistic approaches (semantics) and those who prefer conceptual approaches (Kripke structures, abstract machines). [1]: Not that Britain is too fond of French philosophy, but the Brits had Robin Milner, who is as close to a CS deconstructionist as you could find.
  - willtim 10y ago
    It's worth pointing out that most of the formal methods you have linked to involve contracts or specifications as separate stratified layers written in various logics. No Turing Machines involved. This is essentially functional programming as far as I'm concerned. The advantage of the dependant-type approaches like Coq and Agda, is that the language of proof and implementation is now one of the same, but I was not necessarily advocating their use as you seem to have assumed. Even without dependent types, a total functional program can serve as both an executable specification and a logic with which one can derive proofs from (e.g. via an SMT solver). This is what I meant when I said functional programming is more amenable to formal methods. So any tool that uses dataflow analysis to convert imperative programs into functional ones, or requires me to write functional programs to describe what the imperative program should be doing, doesn't provide a counter argument in my mind. Finally, in my very first comment, I provided a link to a startup who are planning on using FP and SMT solvers for formal verification of blockchain contracts, so watch this space...