We need to think of better tools & practices to secure contracts. It's still all new, there will be issues, there will be improvements. The end goal is worth it IMO. My main Interest in Ethereum (and Maidsafe) like most developers in the community is not so much money but the dream of having a truly decentralised web one day. Impossible? maybe, but I'm willing to try.
It's true of any platform, but Etherium is at a far higher risk of getting hacked because the language is Turing complete. There could conceivably be a smart contract blockchain with a simplified language that was still capable of most of Etherium's good sides with the safety net of static verification tools.
I can easily imagine a system built on a non-Turing complete logical query language that defines data and rules for presentation. You could get pretty far with that. You can't create _any_ application, but calling Turing completeness “essential … for decentralized applications” is incorrect. It's essential for a _subset_ of applications that require Turing completeness.
I've been saying ETH is broken for a while. Its computational ability means contracts _cannot_ be formally verified. This is why I didn't buy into the DAO, and sure enough there's a bug in the DAO (ironically recursion related).
This is why in general software verification doesn't try to come up with languages where all programs are verifiable, but aims to verify specific programs, sometimes regardless of the computational strength. Some programs in Turing complete languages can be verified (but certainly not all), just as some programs in FSM-strength languages can be verified (but certainly not all).
While it is certainly possible that a much bigger subset of, say, FSM programs can be verified than a subset of programs in TC languages, placing the bar at "Turing complete" is somewhat of a red herring.
Indeed, the LANGSEC link in the post[1] seems to understand that, noting that even verifying PDAs is undecidable, but it fails to note that even decidable verification tasks (for FSMs) are very often intractable, which -- for all practical purposes -- is just as bad as being undecidable.
Ethereum, the VM/system is Turing complete, but Ethereum of course is not a language itself. [Correction: EVM code, that is Ethereum VM assembly, is indeed a language. Thus, Ethereum is technically both a VM and a language ("EVM assembly code") - which makes the assertion that "Ethereum is a language" correct after all.]
As far as I understand it, all current Ethereum languages (e.g. Solidity) are also Turing complete, though it should be possible to create a language for Ethereum to produce only algorithms constrained with some level of decidability. This is why Ethereum is likely not doomed yet as some have claimed recently. However, and especially due to The DAO fiasco, it's now a matter of building static verification tools as you suggest, or decidable languages for it, and new cryptosystems may show up before it can get to its first killer app.
Full disclosure: No horses in this race at the moment.
As an aside, I think that everyone posting anything about Bitcoin or Ethereum should be posting a disclosure in each discussion (even an abridged one of some sort, just a couple of characters).
Can someone explain to me how Ethereum fulfils the "dream of having a truly decentralised web"? From my understanding, it just sounds like Bitcoin with programmable contracts tacked on.
How would I run, say, a reddit-like site using Ethereum?
It doesn't. It's hyped up bullshit.
Every Ethereum node runs the exact same code (single threaded too) with heavy computing and storage restraints. There's no sharding or load balancing. Can you run the entire reddit website on a single 90s computer? The answer is no.
Don't get me wrong, Ethereum is an interesting experiment and blockchains are useful for a number of things, but the notion of "lets put everything on the blockchain" is a shitty, terribly inefficient solution looking for a problem.