5 ms·
Rather than fuzzing, why not just implement it in a language with a formal proof like Ada SPARK?
by analognoise 6y ago
Rather than fuzzing, why not just implement it in a language with a formal proof like Ada SPARK?
- iso-8859-1 6y agoSimplicity has a bunch of Coq proofs actually. And Cardano probably has some formal stuff too, but I am not into proof-of-stake.
- DyslexicAtheist 6y agoyou'll still only be as correct as your formal proofs (e.g. using formal proofs isn't a replacement for fuzzing)
- e79 6y agoOn the other hand, fuzzing is only as “correct” as your coverage, properties/assertions, corpus synthesis, etc.
- brian_cloutier 6y agoBecause the outside world sees Ethereum as a business, and is confused why the foundation doesn't do all of these things which would make the "product" better. While the Ethereum Foundation sees Ethereum as an ecosystem, much closer to an open source project, and tries to support people who want to contribute to it. The answer to your question is, nobody has shown up yet who's willing to put in the massive amount of effort required to write the compiler in a formal language. The closest we've gotten to that is an implementation of the evm: https://jellopaper.org/ https://jellopaper.org/