3 ms·
Ethereum is, so far, missing a key element for me to take it really seriously: Formal Methods. There are some small efforts, but I'd rather have formal methods
by nextos 9y ago
Ethereum is, so far, missing a key element for me to take it really seriously: Formal Methods.
There are some small efforts, but I'd rather have formal methods from the beginning, not as an afterthought.
The problem is that market forces favor releasing early rather than releasing correct things. It's the MIT vs NJ paradox again, or worse is better. But this time the potential risks are much bigger.
- drcode 9y agoWell it was a ton of work to get ethereum out the door... Adding a couple more years to formally prove everything first sounds like the perfect way to be stuck in development limbo forever. As you say, formal methods are being applied after the fact to some degree at least.
- nextos 9y agoI think it is a common misconception that formal methods will lead to an extremely slow development cycle. That is only the case if you go for the best guarantee of correctness: Theorem Proving. There are more agile options. For example, model checking all protocols is pretty easy in comparison to theorem proving. Still a significant effort, but perhaps an order of magnitude easier.
- rickycook 9y agowell, that would be tooling though. you wouldn’t say that x86 is missing formal methods therefor you shouldn’t use it right... solidity, etc sure maybe... but at that point, releasing early is probably a good thing so that you can get a whole community working on things and getting ideas and collaboration from a large group of people *edit: unless you mean like geth, or some minimal reference client should be formally proven
- tfha 9y agoWell, a lot of x86 actually does get proven using formal methods. Clearly not all of it, but we've realized that was a bad plan, and that we should go back to formally verifying all of our hardware.