[fab13n]

Functional style doesn't prevent logical errors, but it makes them much easier to find and fix.

Automatic code property verification will probably become pervasive some day, but we're far from there: today's tools require experts to be used, even experts only manage to prove fairly basic properties, and the level of automation is really low. Even writing proof-friendly code and formulating propositions (without proving them) is out of most developers' reach.

[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.