[mbrock]

I think imperativity vs purely functional is mostly a red herring. Lambda functions won't solve your logical mistakes.

What we really need is the ability to automatically verify the possible outcomes of a piece of logic to guarantee crucial safety properties.

That's not an intractable thing. It's possible in many cases today with simple techniques like symbolic execution.

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