> If they didn’t formally verify the smart contract in a way that covers all edge cases including known “exploits” they kinda deserve to have their ethereum transferred to its new holder. Code is law.

It boggles my mind that anyone would want to participate in anything like that, let alone believe it's the future of anything. It's like volunteering to live in a hole in the middle of a WWI no-mans-land, when there are nice homes available in town where you don't have to worry about being killed all the time. It's one thing to be forced to live in a dark forest, it's quite another to choose to live in one (as anything other than the apex predator).

You're forgetting that the biggest community on cryptocurrencies are ancaps thinking they are the apex predators.

According to contract theory, it may not be possible, in practice, to write "complete contracts", that is contracts that specify what is to be done in every possible contingency. See https://en.wikipedia.org/wiki/Complete_contract

"formally verify the contract" it would help if Solidity was as well though out as Ada, and not something more like JS.

I'd even argue that imperative programming is the wrong paradigm for such smart contracts.

Apparently not, as the hard fork into Ethereum and Eth. Classic proves. Once every big stakeholder decides the game isn't in their favor anymore, they change the rules.

It takes an extreme level of hubris to ever think your code covers all edge cases and potential exploits.

>> in a way that covers all edge cases

That is simply not possible. No-one can think of all edge cases.