In addition to this the language is not explicit enough. Even standard Haskell wouldn't be safe enough for a program that manages $250MM directly without safe guards.

In addition to typesafety, it would have to be both explicitly typed at the lowest possible granularity and annotated with pre and post conditions.

Not only did this code allow a bunch of tokens be transferred without compensation, it left the whole accounting system in a corrupted state! One that could have easily been detected and verified at any point.

This line:

    ```
        Transfer(msg.sender, 0, balances[msg.sender]);
    ```

Should have looked like this:

    ```
        // postcondition: balances[msg.sender] == 0
        Transfer(msg.sender, 0, balances[msg.sender]) :: Action<Transfer>;

    // Compiler result:
    // # Error 1: line XX expected type Action<Transfer> but instead got type Transfer
    // # Error 2: line XX violates postcondition, expected balances[msg.sender] == 0, got balances[msg.sender] != 0
    ```

And the whole function 'splitDao' should have a type annotation that completely captures the possible actions it might encompass, and pre- and postconditions that at the very least constrain the result of the function to not corrupt the accounting of the DAO (i.e. it should still have as many tokens as it believes it has).

It's nice that Vitalik Buterin is a genius, but it shows that this guy is only 22 and dropped out of university because anyone with a degree in computer science knows about this stuff and its importance in high reliability systems. He should have known the contract language should have had typechecked side effect and he should have known proper pre- postconditions would have been the least he should have done.