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.