I believe some key root causes are Solidity's and EVM's designs, which encourage a bug-prone programming style.
I'm willing to consider that it's also a _cultural_ thing, beyond the formal features of the VM and its main programming language: Ethereum contract developers don't try hard enough to keep contracts as small (and featureless) as possible. But it doesn't change the bottom line: Ethereum contracts, written with the tools currently available and in the style currently fashionable, are unlikely to be secure.
Object-oriented programming is bad for smart contracts, because encapsulation is bad. As written a long time ago by Joel Spolsky, all non-trivial abstractions end up being leaky abstractions. Encapsulation lets you write much bigger programs which are only slightly more buggy. It doesn't fly for smart contracts, though, because you need zero-defect; if you need encapsulation to keep growing your contract, don't start encapsulating, stop growing your time-bomb of a contract!
Imperative programming is bad for smart contracts, because you need to stay conscious of everything that affects your computation all of the time; shared mutable states make that more difficult. Writing moderately buggy programs in imperative style is easier than functional programming, but confidently writing zero-defect imperative programs is harder than confidently writing zero-defect functional programs (and it pretty much requires to think of your imperative program functionally, anyway).
I believe a sane contract programming language should be (1) purely functional and (2) transactional (when a contract fails, it must roll back any state change or contract calls performed before failing, recursively for contract calls). At some point, being proof-friendly will hopefully become a must, too, but that will require a lot of training for developers, and a lot of progress on theorem provers.
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.
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.
