3 ms·

> it will require formal verification at a scale never before done What problems specific to Ethereum do you see? Formal verification has been applied to compl

> it will require formal verification at a scale never before done What problems specific to Ethereum do you see? Formal verification has been applied to complex domains and large projects before.

mannykannot 9y ago
Depending on who you read, the expectations for Ethereum go all the way up to replacing banking systems, if not beyond, so there does not need to be any problem specific to Ethereum for there to be concerns about the practicality of its verification, though the fact that it is not a well-defined problem domain is itself an issue. Do you have a more restricted expectation of Ethereum's usefulness that implies no more difficulty than the largest formally-verified project that you are aware of? Update: the lower reasonable bound on Ethereum's complexity / usefulness is that it should enable something useful beyond what can be done with Bitcoin, or any other blockchain-based system lacking Turing-complete contracts.
- seanwilson 9y ago
  Why would how useful Ethereum is or could be make a difference? Formal verification has been researched for decades and applied to complex domains like operating systems, hardware, smartcards and huge mathematical proofs already. I don't see why applying it to Ethereum would be a giant leap.
  - mannykannot 9y ago
    We may have a misunderstanding about formality here. While the mere use of defined software development processes has sometimes informally (and confusingly) been called formal, it really isn't. True formal methods involve developing proofs of correctness along with programs, or at least proofs of the absence of certain types of error. Work on this has indeed been going on for decades, and its very limited adoption so far is a testament to its difficulty. Only a tiny fraction of the code in the domains you mention is formally verified, and I notice that banking and finance are not on your list. The answer to "why would how useful Ethereum is or could be make a difference?" is that if Ethereum becomes as useful and important as intended, the size and scope of the problem will be well beyond anything that has been achieved so far. Arguably, given the value at risk, it has already crossed that threshold by a wide margin. There are, however, people working on it, such as at Cardano [1], which is an exciting development. Ultimately, I think it will be more successful than trying to fix Ethereum. If you don't have experience writing formally-verified code, I suggest the F* tutorial [2]. [1] https://www.cardanohub.org/en/home/ https://www.cardanohub.org/en/home/ [2] https://www.fstar-lang.org/tutorial/ https://www.fstar-lang.org/tutorial/
charlesdm 9y ago
There should probably be a set of basic libraries one can use, with certain key functionality that has been audited well (e.g. multisig support)

> it will require formal verification at a scale never before done What problems specific to Ethereum do you see? Formal verification has been applied to complex domains and large projects before.

mannykannot 9y ago

Depending on who you read, the expectations for Ethereum go all the way up to replacing banking systems, if not beyond, so there does not need to be any problem specific to Ethereum for there to be concerns about the practicality of its verification, though the fact that it is not a well-defined problem domain is itself an issue. Do you have a more restricted expectation of Ethereum's usefulness that implies no more difficulty than the largest formally-verified project that you are aware of? Update: the lower reasonable bound on Ethereum's complexity / usefulness is that it should enable something useful beyond what can be done with Bitcoin, or any other blockchain-based system lacking Turing-complete contracts.

seanwilson 9y ago
Why would how useful Ethereum is or could be make a difference? Formal verification has been researched for decades and applied to complex domains like operating systems, hardware, smartcards and huge mathematical proofs already. I don't see why applying it to Ethereum would be a giant leap.
- mannykannot 9y ago
  We may have a misunderstanding about formality here. While the mere use of defined software development processes has sometimes informally (and confusingly) been called formal, it really isn't. True formal methods involve developing proofs of correctness along with programs, or at least proofs of the absence of certain types of error. Work on this has indeed been going on for decades, and its very limited adoption so far is a testament to its difficulty. Only a tiny fraction of the code in the domains you mention is formally verified, and I notice that banking and finance are not on your list. The answer to "why would how useful Ethereum is or could be make a difference?" is that if Ethereum becomes as useful and important as intended, the size and scope of the problem will be well beyond anything that has been achieved so far. Arguably, given the value at risk, it has already crossed that threshold by a wide margin. There are, however, people working on it, such as at Cardano [1], which is an exciting development. Ultimately, I think it will be more successful than trying to fix Ethereum. If you don't have experience writing formally-verified code, I suggest the F* tutorial [2]. [1] https://www.cardanohub.org/en/home/ https://www.cardanohub.org/en/home/ [2] https://www.fstar-lang.org/tutorial/ https://www.fstar-lang.org/tutorial/

charlesdm 9y ago

There should probably be a set of basic libraries one can use, with certain key functionality that has been audited well (e.g. multisig support)