1. Starting from a declarative language (think XML), you might not be as expressive, but you would still have a lot of value and mitigate a lot of the potential problems.
2. Safety properties that fall back on current law could be added in case of dispute.
This scenario would still have great value as a smart contract.
1. XML is just a notation, and being declarative is not in itself a guarantee of easy verification: Prolog is declarative and yet Turing complete (though it's important to note that you don't need to be Turing complete to be hard to verify!). So while declarative is an excellent idea, it doesn't help with the problem of deciding what exactly the language can do to be both useful and relatively easily verifiable.
2. Absolutely, but I think the whole motivation behind projects like Ethereum is to replace the law with algorithms. I think that any computer scientist with a basic understanding of complexity would see why this is impossible, but the idea persists. Eventually, someone who's less ideologically pure would find a way to reconcile the utility of cryptocurrencies with the necessity for human law.
1. It's very hard to create a language that is both restrictive yet useful enough, without it being just as hard to verify (e.g. total-functional languages are not nearly restrictive enough to make some global properties easily provable; the only languages that make this somewhat feasible are finite state machines, and their expressiveness is questionable).
2. Even if that were somehow possible, it wouldn't solve the real problem, which is defining the right safety properties. However you verify safety, the hard problem remains what safety means.