4 ms·

> When are Turing machines ever involved? Most software is written in imperative Turing equivalent languages, so Turing Machines are involved all the time. The

by 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...
- willtim 10y ago
  I can assure you I understand what a Turing machine is. I brought them up because the less powerful abstract machines you mentioned are not sufficient to (fully) express Ethereum or most other mainstream imperative languages. You seem to argue that imperative programming is just as mathematically rigorous as FP, because one can have abstract state machines in mind, yet strongly object when I compare Ethereum to a Turing Machine. You also appear to suggest that formal verification has no problem dealing with computations that require Turing equivalence (by dismissing my point as 'false') and then state that Turing Machines have no place in formal verification. If I sound mixed up it's because I'm trying to make sense of your position. > Everything is "Turing equivalent" This doesn't make any sense. As you say, there are less powerful automatons. A programming language does not need to support universal computation, for example Unix RegEx. I cannot disagree that imperative programming is more popular, but again that is no proof that we are better of using them is we want to easily build correct software.
  - pron 10y ago
    > because the less powerful abstract machines you mentioned are not sufficient to (fully) express Ethereum or most other mainstream imperative languages. No, again -- you are confusing specific machines (like TMs) with abstract state machines. Abstract state machines are a super-set of Turing machines (some are equivalently powerful in terms of computability, albeit "faster" wrt time complexity -- e.g. lambda calculus or RAM machines; others are less powerful). But Ethereum is not a Turing machine, just like Haskell isn't. Turing machines are a very specific thing, like x86 assembly. Ethereum is not based on x86 assembly, just like it isn't based on Turing machines. > but again that is no proof that we are better of using them is we want to easily build correct software. I agree; I didn't say they're any better. But you claimed that FP is better, and there's certainly no evidence to support that. Some extremely powerful formal verification tools, however, currently have no good, production-quality applications for FP.
    - willtim 10y ago
      The confusion here is that you repeatedly seem to misunderstand my point, perhaps that is my fault as I do not have the time to write very carefully (e.g. I've used "Turing Machine" as a cheap shot at imperative programming). You even stated it yourself earlier "because our programs are most certainly not TM-equivalent". If you agree that most programs do not require Turing equivalence, then you must surely understand my main point, which is why provide powerful expressive languages that, for example, do allow Turing complete computations. Does a contract language, or even a systems language need to really support Turing completeness? You seem to argue that it doesn't matter. I think it does.

by willtim 10y ago

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

willtim 10y ago
I can assure you I understand what a Turing machine is. I brought them up because the less powerful abstract machines you mentioned are not sufficient to (fully) express Ethereum or most other mainstream imperative languages. You seem to argue that imperative programming is just as mathematically rigorous as FP, because one can have abstract state machines in mind, yet strongly object when I compare Ethereum to a Turing Machine. You also appear to suggest that formal verification has no problem dealing with computations that require Turing equivalence (by dismissing my point as 'false') and then state that Turing Machines have no place in formal verification. If I sound mixed up it's because I'm trying to make sense of your position. > Everything is "Turing equivalent" This doesn't make any sense. As you say, there are less powerful automatons. A programming language does not need to support universal computation, for example Unix RegEx. I cannot disagree that imperative programming is more popular, but again that is no proof that we are better of using them is we want to easily build correct software.
- pron 10y ago
  > because the less powerful abstract machines you mentioned are not sufficient to (fully) express Ethereum or most other mainstream imperative languages. No, again -- you are confusing specific machines (like TMs) with abstract state machines. Abstract state machines are a super-set of Turing machines (some are equivalently powerful in terms of computability, albeit "faster" wrt time complexity -- e.g. lambda calculus or RAM machines; others are less powerful). But Ethereum is not a Turing machine, just like Haskell isn't. Turing machines are a very specific thing, like x86 assembly. Ethereum is not based on x86 assembly, just like it isn't based on Turing machines. > but again that is no proof that we are better of using them is we want to easily build correct software. I agree; I didn't say they're any better. But you claimed that FP is better, and there's certainly no evidence to support that. Some extremely powerful formal verification tools, however, currently have no good, production-quality applications for FP.
  - willtim 10y ago
    The confusion here is that you repeatedly seem to misunderstand my point, perhaps that is my fault as I do not have the time to write very carefully (e.g. I've used "Turing Machine" as a cheap shot at imperative programming). You even stated it yourself earlier "because our programs are most certainly not TM-equivalent". If you agree that most programs do not require Turing equivalence, then you must surely understand my main point, which is why provide powerful expressive languages that, for example, do allow Turing complete computations. Does a contract language, or even a systems language need to really support Turing completeness? You seem to argue that it doesn't matter. I think it does.