[AstralStorm]

Why would anyone want code that is not mathematically proven to become law?

Yes, even with modern automatic theorem provers it is a bit torturous. But people are even going so far as writing a mathematically proven safe kernel (1) and Ethereum is much smaller and simpler.

(1) https://sel4.systems/

[larkery]

I think you raise a good question; I further wonder whether the provability of outcomes is even sufficient to justify the kind of total procedural adherence which the ethereum folks (until recently!) advocated.

In normal contract law that doesn't have a blockchain in it there is a special moral "backstop" where a judge may find a contract to be unconscionable. An unconscionable contract may contain nothing forbidden by statute, but if it is found to be profoundly unjust in terms of its outcomes (not due to change in circumstance, but as a result of its formulation), then a judge can call the contract unconscionable and it is void.

This kind of latitude is really valuable, as it recognises the fact that things are pretty complicated and that in the end the law is there to ensure justice, not to mechanically interpret a set of rules.

So, even if you have a smart contract (or as I would call it "program") which can be proven to work a certain way, that may not be enough to guarantee that it is not going to give rise to bad outcomes. For example, say we have a proof showing that the program obeys some invariants, and one may even have such a proof generated automatically. This makes us feel confident - let us irreversibly bind our future actions to the output of the program! Blockchains be praised!

However, if the real invariant being aimed for is that the program's execution is "justice-preserving" (and I would say this is a good aim), then there is a grounding problem we have missed, where the prover needs to specify formally the nature of a just situation or action.

I believe a large number of person-years have already been spent on attempts to derive such an "ethics predicate", but if anyone has found it they have not yet bothered to demonstrate it. As a result if we wish to pursue justice, we end up falling back to the position taken by the ordinary law, and we might wonder quite why we decided to use 51% of all computing power for the rest of time to keep a ledger intact in the first place.

[vintermann]

> This kind of latitude is really valuable, as it recognises the fact that things are pretty complicated and that in the end the law is there to ensure justice, not to mechanically interpret a set of rules.

It's also entirely dependent on judges being nice and reasonable people, who will judge according to common sense standards of "what is right" shared by a solid majority. This just isn't true. If anything, judges are likely to be less reasonable than random regular people, because

1. They have an education where argument is treated as a sport, and objective measures of bias or correctness play little part.

2. They belong to a class who firmly believe (and society backs them up on it and tries as hard as it can to make it reality) that their opinions are worth more than ordinary people's.

That was always my problem with libertarians, their eagerness look to the legal system to solve social problems (contracts, etc.). The judicial branch is the worst of all branches of government. Sensible people don't go there to get justice, it's where you go when you've given up getting justice any other way.

A judge is just as likely (if not more) to protect an unjust order as to overturn it when it's really called for. Ethereum provides a way to guarantee desirable outcomes without such arbitrariness (in the very literal sense). It failed to do so with the DAO, but at least there, bugs can be fixed. It's much harder to fix unjust judges.

[chopin]

Proven against what? The intentions of coder? In that case the intentions need to be codified. With that, we are back to square one I think.

[drdeca]

If a contract is sufficiently simple, it seems to me like it could make sense.

However, I do think it is, or perhaps, would have been, important to put a lot of focus on moving to mathematically proven contracts.