3 ms·

Formal verification can be layered on top. One simple use case is as a way of proving termination, greatly mitigating gas-related issues. Another use case is pr

by panic 10y ago

Formal verification can be layered on top. One simple use case is as a way of proving termination, greatly mitigating gas-related issues. Another use case is proving specific properties – for example, “if all participants collude, they can get their money out in all cases”, or “if you send your tokens A to this contract, you are guaranteed to either get the amount of token B that you want or be able to fully refund yourself”. Or “this contract fits into a restricted subset of Solidity that makes re-entrancy, gas issues and call stack issues impossible”. Why not restrict the entire language instead of trying to verify that a program fits into a safe subset? What practical uses are there for general recursion and unbounded gas usage in the context of smart contracts (not to mention multiple inheritance, inline bytecode assembly, and the many other complex features of Solidity)?

pron 10y ago
Because: 1. It's very hard to create a language that is both restrictive yet useful enough, without it being just as hard to verify (e.g. total-functional languages are not nearly restrictive enough to make some global properties easily provable; the only languages that make this somewhat feasible are finite state machines, and their expressiveness is questionable). 2. Even if that were somehow possible, it wouldn't solve the real problem, which is defining the right safety properties. However you verify safety, the hard problem remains what safety means.
- db3d 10y ago
  1. Starting from a declarative language (think XML), you might not be as expressive, but you would still have a lot of value and mitigate a lot of the potential problems. 2. Safety properties that fall back on current law could be added in case of dispute. This scenario would still have great value as a smart contract.
  - pron 10y ago
    1. XML is just a notation, and being declarative is not in itself a guarantee of easy verification: Prolog is declarative and yet Turing complete (though it's important to note that you don't need to be Turing complete to be hard to verify!). So while declarative is an excellent idea, it doesn't help with the problem of deciding what exactly the language can do to be both useful and relatively easily verifiable. 2. Absolutely, but I think the whole motivation behind projects like Ethereum is to replace the law with algorithms. I think that any computer scientist with a basic understanding of complexity would see why this is impossible, but the idea persists. Eventually, someone who's less ideologically pure would find a way to reconcile the utility of cryptocurrencies with the necessity for human law.

by panic 10y ago

pron 10y ago

Because: 1. It's very hard to create a language that is both restrictive yet useful enough, without it being just as hard to verify (e.g. total-functional languages are not nearly restrictive enough to make some global properties easily provable; the only languages that make this somewhat feasible are finite state machines, and their expressiveness is questionable). 2. Even if that were somehow possible, it wouldn't solve the real problem, which is defining the right safety properties. However you verify safety, the hard problem remains what safety means.

db3d 10y ago
1. Starting from a declarative language (think XML), you might not be as expressive, but you would still have a lot of value and mitigate a lot of the potential problems. 2. Safety properties that fall back on current law could be added in case of dispute. This scenario would still have great value as a smart contract.
- pron 10y ago
  1. XML is just a notation, and being declarative is not in itself a guarantee of easy verification: Prolog is declarative and yet Turing complete (though it's important to note that you don't need to be Turing complete to be hard to verify!). So while declarative is an excellent idea, it doesn't help with the problem of deciding what exactly the language can do to be both useful and relatively easily verifiable. 2. Absolutely, but I think the whole motivation behind projects like Ethereum is to replace the law with algorithms. I think that any computer scientist with a basic understanding of complexity would see why this is impossible, but the idea persists. Eventually, someone who's less ideologically pure would find a way to reconcile the utility of cryptocurrencies with the necessity for human law.