3 ms·

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 operatin

• 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/