There is a new decidable language that compiles to EVM bytecode: https://github.com/ethereum/viper Visually it looks similar to Python. The language is not turing complete, and one of the advantages of this is it's easier write bug free code and easier to verify that the code is doing what you think it's doing.
The reason why the entire EVM is turing complete (and not more limited) is because making it decidable instead is harder than making it Turing complete and would have made the protocol more complex: https://github.com/ethereum/wiki/wiki/White-Paper#computatio...
A Turing-complete language is base layer: you can build any paradigm you want on top.
Since the hack, various small improvements have been made to Solidity, the Foundation hired someone to work full-time on formal verification, there's the new Viper language which is easier to verify, and the community has gotten a lot more serious about coding standards and security audits.
TheDAO very explicitly states that you can't do this: "Your use of the Software does not, in and of itself, create a legally binding contract in any jurisdiction and does not establish a lawyer-client relationship. Your communication with a non-lawyer will not be subject to the attorney-client privilege and (depending on your jurisdiction) may not be entitled to protection as confidential communication."
Honestly, though, I have absolutely no idea what would happen in a legal case involving 'smart contracts', as I don't think there's any precedent involving treating computer programs as contracts.
It turns out the code of a smart contract doesn't override the legal system.
Smart contracts aren't legal contracts, though they may be evidence of the existence and content of one.
Of course, strictly speaking that's true of the written documentation of a contract, too.
It would be an interesting case, for sure.
The issue is, the person wasn't a 'hacker' in any meaningful sense of the word.
Etherium claims to be "a decentralized platform that runs smart contracts: applications that run exactly as programmed without any possibility of downtime, censorship, fraud or third party interference" (from etherium.org). That is, an Etherium program doesn't implement a written contract, it is the contract.
Despite this lofty goal, the core team saw fit to hard-fork the chain because they didn't like how a particular program was executing. The claim that the 'hacker' had 'stolen' funds from theDAO is ridiculous - you can only steal what doesn't belong to you, and ownership of theDAO's Ether is defined by the program itself!
More broadly, the hard-fork seems to imply that an Etherium contract is really made up of two contracts. One contract is the program itself, which explicitly spells out what is and not allowed. The other contract is an implicit understanding of what the program 'should' do, and exists only in the minds of the creators of the contract. The issue arises when this implicit 'contract' is used to override the real contract - flying in the face of how Etherium claims to work.
A much better solution would have been to try to address the underlying issues in Solidity - perhaps requiring future contracts to explicitly allow recursion? I personally question the decision to use a Turing-complete language to express contracts in the first place.