This is an awesome post.
It went a bit over my head! I'm excited to sit down and really study this and try to parse it out really well.
I was kind of disappointed in ETH's fork, because it seems to me that the only way that we're going to achieve reliable smart contracts is by trial and error.
I think that The DAO made a mistake, and got too big for its britches. For the same reason that we didn't put a human on the first rocket to the moon, it was a mistake to invest as much money was in The DAO.
But humans will be humans. We may lose a few monkeys along the way. But the beauty of free software is that it liberates us from creating products -- instead, we are all computer scientists, working together to discover what computers are capable of.
Along the way we're going to find cool new ways of expressing contracts. I totally agree that the optimal smart contract language has likely not been invented yet.
Awesome post. Thanks again.