4 ms·

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

by 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.
  - pron 10y ago
    Oh, you are right that finite-state machines make automated verification easier (assuming that by Turing machine you meant Turing complete). However, some people are under the impression that other sub-Turing-complete languages (in particular, total functional programs) are easier to verify than programs in Turing-complete languages. This is false. The only class of languages that are practically "easy" to verify are finite state machines (well, if you call being PSPACE-complete easy; even that is exponential in the program's size!). This is easy to prove (in fact, it is a simple corrolary of the time hierarchy theorem and its proof). In particular, it is trivial to show that the problem of verifying a program in a total language is harder than any problem with a computable complexity bound, i.e. it's complexity is non-computable, i.e. it has "busy beaver" complexity[1]. I'm giving a talk on this precise subject next month at Curry On (http://curry-on.org/2016/sessions/why-writing-correct-software-is-hard-and-why-math-alone-wont-help-us.html http://curry-on.org/2016/sessions/why-writing-correct-softwa...) [1]: The difference, therefore, between verification of Turing-complete programs and total programs is that the cost of verifying the former in the general case is infinite, while the cost of the other grows like some function that is larger than any function we can ever compute. From the perspective of computing power, both are equally beyond reach.
    - willtim 10y ago
      That looks like a great talk, I hope it will be recorded.

by willtim 10y ago

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.
- pron 10y ago
  Oh, you are right that finite-state machines make automated verification easier (assuming that by Turing machine you meant Turing complete). However, some people are under the impression that other sub-Turing-complete languages (in particular, total functional programs) are easier to verify than programs in Turing-complete languages. This is false. The only class of languages that are practically "easy" to verify are finite state machines (well, if you call being PSPACE-complete easy; even that is exponential in the program's size!). This is easy to prove (in fact, it is a simple corrolary of the time hierarchy theorem and its proof). In particular, it is trivial to show that the problem of verifying a program in a total language is harder than any problem with a computable complexity bound, i.e. it's complexity is non-computable, i.e. it has "busy beaver" complexity[1]. I'm giving a talk on this precise subject next month at Curry On (http://curry-on.org/2016/sessions/why-writing-correct-software-is-hard-and-why-math-alone-wont-help-us.html http://curry-on.org/2016/sessions/why-writing-correct-softwa...) [1]: The difference, therefore, between verification of Turing-complete programs and total programs is that the cost of verifying the former in the general case is infinite, while the cost of the other grows like some function that is larger than any function we can ever compute. From the perspective of computing power, both are equally beyond reach.
  - willtim 10y ago
    That looks like a great talk, I hope it will be recorded.