5 ms·

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

by 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...

pron 10y ago
> No Turing Machines involved. When are Turing machines ever involved? Verification tools often make use of abstract state machines as the subject of their study. I am not aware of a single one that deals with Turing machines (nor am I aware of a single TM programming language being used in the industry). TMs serve an important role in theoretical computer science, in automata theory and complexity theory, but not in verification or PL. > This is essentially functional programming as far as I'm concerned. It isn't. Logic was applied to programs long before FP was in vogue. > 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, Two things. First, you can implement a system in Isabelle, too. Second, that advantage -- if it is one -- is rather theoretical at this point. Dependently typed languages have never been used outside of the lab, and have never been used in a large project. The approach, BTW, has plenty of disadvantages. First, the languages are very hard to learn, and require some very exotic, obscure math; second, some very important properties like time and space complexity -- that are often just as essential as logical correctness for those application where correctness matters most -- are hard to express, and there's no consensus yet on how to best reason about them. In short, dependent type approaches may one day be useful, but in general, we're not sure exactly how to use them yet. > a total functional program can serve as both an executable specification and a logic with which one can derive proofs from That is absolutely true, but this has some very severe disadvantages as well. > so watch this space... I have no doubt. But you should be aware that FP approaches to verification are just some of the many avenues in verification research these days, and are not generally accepted to be the most promising ones. In addition, unlike other approaches, they have pretty much never been put to the test outside the lab. Finally, SMT solvers are successfully used to verify Java programs (with JML specifications), and in the research world, Microsoft's Dafny[1] -- an imperative, non-functional (I think) language -- is a very popular choice in verification challenges (alongside tools like KIV[2] and Why3[3]). They also, I think, serve as the core proof method of SPARK Ada, a heavy duty verifiable language, with a good track record over many years in the industry. [1]: http://research.microsoft.com/en-us/projects/dafny/ http://research.microsoft.com/en-us/projects/dafny/ [2]: http://www.isse.uni-augsburg.de/en/software/kiv/ http://www.isse.uni-augsburg.de/en/software/kiv/ [3]: http://why3.lri.fr/ http://why3.lri.fr/
- willtim 10y ago
  > When are Turing machines ever involved? Most software is written in imperative Turing equivalent languages, so Turing Machines are involved all the time. The fact that most verification software is not capable of dealing with them, demonstrates a language issue. Which is the point I have been trying to make. > It isn't. Logic was applied to programs long before FP was in vogue. I'm advocating modelling contracts with Logic, instead of Turing Machines as used by Ethereum. I didn't mean to create a tribal boundary by using the term FP.
  - pron 10y ago
    > Most software is written in imperative Turing equivalent languages, so Turing Machines are involved all the time. I don't understand what that means. Everything is "Turing equivalent" in some sense[0]. It's like saying that since every language can be compiled to C, then C is "involved all the time". That would even be more accurate, because our programs are most certainly not TM-equivalent. Proof: the asymptotic complexity of a real program and that of a Turing machine for most algorithms differs by a power of 2 or 3. Therefore, programs and TMs cannot possibly be equivalent. If you had said RAM machines at least you would have been somewhere in the ballpark, and RAM machines are not Turing machines (see https://en.wikipedia.org/wiki/Random-access_machine https://en.wikipedia.org/wiki/Random-access_machine). > The fact that most verification software is not capable of dealing with them, demonstrates a language issue. But that is not a fact, because 99% of the thousands of very real, verified production systems being constantly worked on are written in imperative languages, and roughly 0-1% is written in functional languages. Quite the contrary, verification software handles imperative programs better than functional programs. You don't have to take my word for it. See what one Xavier Leroy (author of CompCert) says on the issue here[1] and here[2]. So far, verification in functional languages requires inordinate effort. The question of how much verification is tied to language is very much an open question. > I'm advocating modelling contracts with Logic, instead of Turing Machines as used by Ethereum. I wonder what you'd say about temporal logic, which is not only the most popular logic in software verification but one that models state machines. As to Turing machines, I don't think you understand what they are. A Turing machine is one particular automaton, a particular instance of an abstract state machine, and a universal computational model, which is usually applied directly only in computational complexity theory, where it serves as a common cost model. The lambda calculus is a rewriting system (typed versions of which can be tied to one particular kind of logical reasoning via the C-H correspondence), another universal model of computation, and -- guess what -- another instance of an (ND) abstract state machine! In short there are many concepts here that you mix up. Turing machines, however, are one concept that is completely absent from both PLs and software verification (where it tends to turn up only in the marketing speech of some FP advocates). No one programs Turing machines. Program logics most certainly apply to imperative languages, and in fact, this is -- to date -- where they are most used, and quite successfully. [0]: And if you're referring to total languages then you're confusing things further. Totality has little effect on verification; it is required in order to not introduce logical inconsistencies in typed lambda calculus, and is only relevant when dependently typed languages are used to prove general mathematical theorems -- not verify programs. [1]: http://events.inf.ed.ac.uk/Milner2012/X_Leroy-html5-mp4.html http://events.inf.ed.ac.uk/Milner2012/X_Leroy-html5-mp4.html [2]: http://events.inf.ed.ac.uk/Milner2012/Monday_Panel-html5-mp4.html http://events.inf.ed.ac.uk/Milner2012/Monday_Panel-html5-mp4...

by willtim 10y ago

pron 10y ago

> No Turing Machines involved. When are Turing machines ever involved? Verification tools often make use of abstract state machines as the subject of their study. I am not aware of a single one that deals with Turing machines (nor am I aware of a single TM programming language being used in the industry). TMs serve an important role in theoretical computer science, in automata theory and complexity theory, but not in verification or PL. > This is essentially functional programming as far as I'm concerned. It isn't. Logic was applied to programs long before FP was in vogue. > 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, Two things. First, you can implement a system in Isabelle, too. Second, that advantage -- if it is one -- is rather theoretical at this point. Dependently typed languages have never been used outside of the lab, and have never been used in a large project. The approach, BTW, has plenty of disadvantages. First, the languages are very hard to learn, and require some very exotic, obscure math; second, some very important properties like time and space complexity -- that are often just as essential as logical correctness for those application where correctness matters most -- are hard to express, and there's no consensus yet on how to best reason about them. In short, dependent type approaches may one day be useful, but in general, we're not sure exactly how to use them yet. > a total functional program can serve as both an executable specification and a logic with which one can derive proofs from That is absolutely true, but this has some very severe disadvantages as well. > so watch this space... I have no doubt. But you should be aware that FP approaches to verification are just some of the many avenues in verification research these days, and are not generally accepted to be the most promising ones. In addition, unlike other approaches, they have pretty much never been put to the test outside the lab. Finally, SMT solvers are successfully used to verify Java programs (with JML specifications), and in the research world, Microsoft's Dafny[1] -- an imperative, non-functional (I think) language -- is a very popular choice in verification challenges (alongside tools like KIV[2] and Why3[3]). They also, I think, serve as the core proof method of SPARK Ada, a heavy duty verifiable language, with a good track record over many years in the industry. [1]: http://research.microsoft.com/en-us/projects/dafny/ http://research.microsoft.com/en-us/projects/dafny/ [2]: http://www.isse.uni-augsburg.de/en/software/kiv/ http://www.isse.uni-augsburg.de/en/software/kiv/ [3]: http://why3.lri.fr/ http://why3.lri.fr/

willtim 10y ago
> When are Turing machines ever involved? Most software is written in imperative Turing equivalent languages, so Turing Machines are involved all the time. The fact that most verification software is not capable of dealing with them, demonstrates a language issue. Which is the point I have been trying to make. > It isn't. Logic was applied to programs long before FP was in vogue. I'm advocating modelling contracts with Logic, instead of Turing Machines as used by Ethereum. I didn't mean to create a tribal boundary by using the term FP.
- pron 10y ago
  > Most software is written in imperative Turing equivalent languages, so Turing Machines are involved all the time. I don't understand what that means. Everything is "Turing equivalent" in some sense[0]. It's like saying that since every language can be compiled to C, then C is "involved all the time". That would even be more accurate, because our programs are most certainly not TM-equivalent. Proof: the asymptotic complexity of a real program and that of a Turing machine for most algorithms differs by a power of 2 or 3. Therefore, programs and TMs cannot possibly be equivalent. If you had said RAM machines at least you would have been somewhere in the ballpark, and RAM machines are not Turing machines (see https://en.wikipedia.org/wiki/Random-access_machine https://en.wikipedia.org/wiki/Random-access_machine). > The fact that most verification software is not capable of dealing with them, demonstrates a language issue. But that is not a fact, because 99% of the thousands of very real, verified production systems being constantly worked on are written in imperative languages, and roughly 0-1% is written in functional languages. Quite the contrary, verification software handles imperative programs better than functional programs. You don't have to take my word for it. See what one Xavier Leroy (author of CompCert) says on the issue here[1] and here[2]. So far, verification in functional languages requires inordinate effort. The question of how much verification is tied to language is very much an open question. > I'm advocating modelling contracts with Logic, instead of Turing Machines as used by Ethereum. I wonder what you'd say about temporal logic, which is not only the most popular logic in software verification but one that models state machines. As to Turing machines, I don't think you understand what they are. A Turing machine is one particular automaton, a particular instance of an abstract state machine, and a universal computational model, which is usually applied directly only in computational complexity theory, where it serves as a common cost model. The lambda calculus is a rewriting system (typed versions of which can be tied to one particular kind of logical reasoning via the C-H correspondence), another universal model of computation, and -- guess what -- another instance of an (ND) abstract state machine! In short there are many concepts here that you mix up. Turing machines, however, are one concept that is completely absent from both PLs and software verification (where it tends to turn up only in the marketing speech of some FP advocates). No one programs Turing machines. Program logics most certainly apply to imperative languages, and in fact, this is -- to date -- where they are most used, and quite successfully. [0]: And if you're referring to total languages then you're confusing things further. Totality has little effect on verification; it is required in order to not introduce logical inconsistencies in typed lambda calculus, and is only relevant when dependently typed languages are used to prove general mathematical theorems -- not verify programs. [1]: http://events.inf.ed.ac.uk/Milner2012/X_Leroy-html5-mp4.html http://events.inf.ed.ac.uk/Milner2012/X_Leroy-html5-mp4.html [2]: http://events.inf.ed.ac.uk/Milner2012/Monday_Panel-html5-mp4.html http://events.inf.ed.ac.uk/Milner2012/Monday_Panel-html5-mp4...