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.
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.
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.
Why not restrict the entire language instead of trying to verify that a program fits into a safe subset? What practical uses are there for general recursion and unbounded gas usage in the context of smart contracts (not to mention multiple inheritance, inline bytecode assembly, and the many other complex features of Solidity)?