5 ms·

The belief that Turing machines aren't amenable to formal verification is a hobgoblin that shows up in every thread like this, but it's not real. Of course the

by mbrock 9y ago

The belief that Turing machines aren't amenable to formal verification is a hobgoblin that shows up in every thread like this, but it's not real. Of course there are limited formalisms that make certain types of verification easier, but proving programs has been possible since, like, the 1960s. A multisig, for example, has a finite number of states when considered under symbolic execution. A model checker can rip through it and prove whatever properties you want. Is the Ethereum world right now full of buggy contracts that haven't been proven correct? Yes, absolutely. It's a disaster. But it's a disaster that points the way fairly straightforwardly. Should Ethereum not have been launched until it had solid methods for auditing and proving? Maybe, but that's not how the world works, typically. Worse is better and all that.

merijnv 9y ago
Sure, you CAN verify Turing machines, but verifying languages that AREN'T Turing complete is sufficiently simpler. So why not make your verification work easier by using a total language? The only real argument against that would be "we can't do what we want in a total language". I don't buy the argument that what people want to do with smart contracts requires Turing-completeness. In fact, as time goes on I become more and more convinced that Turing completeness is highly overrated. Almost all code wants to do finite and/or structurally inductive operations. The only case that doesn't fall in that are things like request loops where you want to "infinitely" wait, process request, loop back to waiting. But even those things can be done in total languages via co-induction, so exactly why do we want to make our analysis/verification work more difficult by using a non-total language for things like Ethereum?
- mbrock 9y ago
  The real answer is probably that total languages are obscure and the Ethereum inventors didn't know about them so they chose a simple and ordinary stack machine. But those total systems are, of course, subsets of Ethereum, which means that if you write your program in an obviously finite way, you can use the same inductive proofs you would use for a total language. Turing completeness makes it hard to prove properties automatically about arbitrary programs, but you can still prove properties about specific programs. I'm pretty sure that MOST research on program verification has been done in the context of Turing complete systems, from the work of Floyd and Hoare, to the symbolic execution of Deutsch and King, to temporal logic, TLA+, etc.
  - seanwilson 9y ago
    > The real answer is probably that total languages are obscure and the Ethereum inventors didn't know about them so they chose a simple and ordinary stack machine. I'm not an expert on Ethereum, but even if they did pick a total language, how would you deal with bounding the CPU cost of complex contracts? Even if you could formally verify a loop would eventually terminate, wouldn't long running loops or those with expensive computations have bad impacts on the network? Their "gas" system is their way of dealing with that and perhaps you would still need something similar even with a total language. I can't think of program verification research where both termination and CPU cost is verified. I can think of some papers that deal with identifying Big Oh growth rates though. Either way, smart contracts sound like one of the top tier areas where you want strong static typing that has a route to be formally verified.
    - grogenaut 9y ago
      I'm not sure static typing is tied to formal verification. In fact if you think about it most proofs are basically typeless I a lot of cases.
      - seanwilson 9y ago
        What proof systems are you thinking about? Strong static types seem the most natural way to introduce formal verification into mainstream programming to me.
        grogenaut 9y ago
        Well general mathmatecial proofs or TLA+... or would it be better to define "integer" as a strong type which I'm willing to concede.
        seanwilson 9y ago
        I don't feel there's much difference between e.g. the Coq way where types are used to bake specifications + proofs into the program and the Isabelle way where you write a program with less complex types and prove properties about the program after the fact. General mathematical proofs? If you mean paper proofs they wouldn't be considered formal as they don't go down to the axiom level.
- ekidd 9y ago
  Corecursion and codata are cool, and I would trust Solidity vastly more if it were a "total" functional language with no mutable state and aggressive type checking. Or if it were something more like https://www.idris-lang.org/ https://www.idris-lang.org/ , where I had abundant tools to rigorously prove that nobody could steal my money. Basically, if I'm going to spend even 5 minutes playing with smart contracts, I want to feel like the language designers were incredibly paranoid and aware of just how good modern languages can be at provability and security.
  - mbrock 9y ago
    If you're competent with proofs in Idris, you can write your EVM programs as an Idris DSL. But, I mean, there's no proof that the Idris compiler does what it's supposed to do, so you'd still have a huge trusted base.
    - ekidd 9y ago
      > If you're competent with proofs in Idris, you can write your EVM programs as an Idris DSL. Yeah, all my formal proof experience is with Coq, which is just a bit too idiosyncratic and difficult for this sort of thing. But I seem to remember that—especially if you're willing to certify specific results, and not necessarily the program in general—you can make your trusted computing base very small indeed. I mean, if the CompCert C compiler can be as thoroughly verified as it is (http://compcert.inria.fr/compcert-C.html http://compcert.inria.fr/compcert-C.html), there's no reason why it shouldn't be possible to verify smart contracts.
      - seanwilson 9y ago
        > I mean, if the CompCert C compiler can be as thoroughly verified as it is (http://compcert.inria.fr/compcert-C.html http://compcert.inria.fr/compcert-C.html), there's no reason why it shouldn't be possible to verify smart contracts. Hmm, so from the smart contract examples I've seen, I would have thought writing them in something like Coq would be quite feasible. The code examples I've seen tend to only have simple loops if any, basic conditions and the code is short (e.g. compared to something like web development or mobile apps). Writing anything inside a theorem prover is very challenging though but it seems a compelling application. If you were implementing a smart contract in something like Coq, I'd be interested to read about what kind of specifications you would typically want to verify. I guess properties like "the owner of this wallet cannot be changed" and "the owner of this wallet can only accept money but not give it away" would be good ones.
KirinDave 9y ago
Etherium should have launched with a language that wasn't a high-school-extra-cirricular-level in terms of construction and consideration. Solidity doesn't have a problem with formal verification of programs. Check their bug tracker: you can't even trust the runtime to do what it claims to do. On several levels.
empath75 9y ago
> Should Ethereum not have been launched until it had solid methods for auditing and proving? Maybe, but that's not how the world works, typically. Worse is better and all that. As a platform for experimentation that's fine. As a platform for doing real things with meaningful amounts of money, it's madness.
- mbrock 9y ago
  Madness indeed. For better or for worse, silly experiments in this industry often turn out to win. According to the "Worse is Better" theory, that's partly because they ship much faster than the projects that want to get everything right, and they're also easier for most people to understand. You could put a team of Ph.D's on inventing a really amazing smart contract formalism based on higher-order zygomorphic type theory, but if only five people in the universe understood it, we wouldn't be talking about it.
naasking 9y ago
> It's a disaster. But it's a disaster that points the way fairly straightforwardly. A disaster that could have been avoided if they had done a little more research on security and smart contract languages: http://lambda-the-ultimate.org/node/5003 http://lambda-the-ultimate.org/node/5003 Solidity is still clearly focused on programming productivity instead of contract soundness. The built in dynamism is proof of this.

by mbrock 9y ago

merijnv 9y ago

Sure, you CAN verify Turing machines, but verifying languages that AREN'T Turing complete is sufficiently simpler. So why not make your verification work easier by using a total language? The only real argument against that would be "we can't do what we want in a total language". I don't buy the argument that what people want to do with smart contracts requires Turing-completeness. In fact, as time goes on I become more and more convinced that Turing completeness is highly overrated. Almost all code wants to do finite and/or structurally inductive operations. The only case that doesn't fall in that are things like request loops where you want to "infinitely" wait, process request, loop back to waiting. But even those things can be done in total languages via co-induction, so exactly why do we want to make our analysis/verification work more difficult by using a non-total language for things like Ethereum?

mbrock 9y ago
The real answer is probably that total languages are obscure and the Ethereum inventors didn't know about them so they chose a simple and ordinary stack machine. But those total systems are, of course, subsets of Ethereum, which means that if you write your program in an obviously finite way, you can use the same inductive proofs you would use for a total language. Turing completeness makes it hard to prove properties automatically about arbitrary programs, but you can still prove properties about specific programs. I'm pretty sure that MOST research on program verification has been done in the context of Turing complete systems, from the work of Floyd and Hoare, to the symbolic execution of Deutsch and King, to temporal logic, TLA+, etc.
- seanwilson 9y ago
  > The real answer is probably that total languages are obscure and the Ethereum inventors didn't know about them so they chose a simple and ordinary stack machine. I'm not an expert on Ethereum, but even if they did pick a total language, how would you deal with bounding the CPU cost of complex contracts? Even if you could formally verify a loop would eventually terminate, wouldn't long running loops or those with expensive computations have bad impacts on the network? Their "gas" system is their way of dealing with that and perhaps you would still need something similar even with a total language. I can't think of program verification research where both termination and CPU cost is verified. I can think of some papers that deal with identifying Big Oh growth rates though. Either way, smart contracts sound like one of the top tier areas where you want strong static typing that has a route to be formally verified.
  - grogenaut 9y ago
    I'm not sure static typing is tied to formal verification. In fact if you think about it most proofs are basically typeless I a lot of cases.
    - seanwilson 9y ago
      What proof systems are you thinking about? Strong static types seem the most natural way to introduce formal verification into mainstream programming to me.
      - grogenaut 9y ago
        Well general mathmatecial proofs or TLA+... or would it be better to define "integer" as a strong type which I'm willing to concede.
        seanwilson 9y ago
        I don't feel there's much difference between e.g. the Coq way where types are used to bake specifications + proofs into the program and the Isabelle way where you write a program with less complex types and prove properties about the program after the fact. General mathematical proofs? If you mean paper proofs they wouldn't be considered formal as they don't go down to the axiom level.
ekidd 9y ago
Corecursion and codata are cool, and I would trust Solidity vastly more if it were a "total" functional language with no mutable state and aggressive type checking. Or if it were something more like https://www.idris-lang.org/ https://www.idris-lang.org/ , where I had abundant tools to rigorously prove that nobody could steal my money. Basically, if I'm going to spend even 5 minutes playing with smart contracts, I want to feel like the language designers were incredibly paranoid and aware of just how good modern languages can be at provability and security.
- mbrock 9y ago
  If you're competent with proofs in Idris, you can write your EVM programs as an Idris DSL. But, I mean, there's no proof that the Idris compiler does what it's supposed to do, so you'd still have a huge trusted base.
  - ekidd 9y ago
    > If you're competent with proofs in Idris, you can write your EVM programs as an Idris DSL. Yeah, all my formal proof experience is with Coq, which is just a bit too idiosyncratic and difficult for this sort of thing. But I seem to remember that—especially if you're willing to certify specific results, and not necessarily the program in general—you can make your trusted computing base very small indeed. I mean, if the CompCert C compiler can be as thoroughly verified as it is (http://compcert.inria.fr/compcert-C.html http://compcert.inria.fr/compcert-C.html), there's no reason why it shouldn't be possible to verify smart contracts.
    - seanwilson 9y ago
      > I mean, if the CompCert C compiler can be as thoroughly verified as it is (http://compcert.inria.fr/compcert-C.html http://compcert.inria.fr/compcert-C.html), there's no reason why it shouldn't be possible to verify smart contracts. Hmm, so from the smart contract examples I've seen, I would have thought writing them in something like Coq would be quite feasible. The code examples I've seen tend to only have simple loops if any, basic conditions and the code is short (e.g. compared to something like web development or mobile apps). Writing anything inside a theorem prover is very challenging though but it seems a compelling application. If you were implementing a smart contract in something like Coq, I'd be interested to read about what kind of specifications you would typically want to verify. I guess properties like "the owner of this wallet cannot be changed" and "the owner of this wallet can only accept money but not give it away" would be good ones.

KirinDave 9y ago

Etherium should have launched with a language that wasn't a high-school-extra-cirricular-level in terms of construction and consideration. Solidity doesn't have a problem with formal verification of programs. Check their bug tracker: you can't even trust the runtime to do what it claims to do. On several levels.

empath75 9y ago

> Should Ethereum not have been launched until it had solid methods for auditing and proving? Maybe, but that's not how the world works, typically. Worse is better and all that. As a platform for experimentation that's fine. As a platform for doing real things with meaningful amounts of money, it's madness.

mbrock 9y ago
Madness indeed. For better or for worse, silly experiments in this industry often turn out to win. According to the "Worse is Better" theory, that's partly because they ship much faster than the projects that want to get everything right, and they're also easier for most people to understand. You could put a team of Ph.D's on inventing a really amazing smart contract formalism based on higher-order zygomorphic type theory, but if only five people in the universe understood it, we wouldn't be talking about it.

naasking 9y ago

> It's a disaster. But it's a disaster that points the way fairly straightforwardly. A disaster that could have been avoided if they had done a little more research on security and smart contract languages: http://lambda-the-ultimate.org/node/5003 http://lambda-the-ultimate.org/node/5003 Solidity is still clearly focused on programming productivity instead of contract soundness. The built in dynamism is proof of this.