[mbrock]

I think basic properties would go a hell of a long way, especially combined with a cultural inclination toward simple contracts.

I don't think proving basic security properties of simple contracts is far off. Solidity itself has recently gained the ability to statically guarantee the absence of some assertions, using the Z3 SMT solver.