Deconstructing the DAO Attack: A Brief Code Tour

First of all, end-to-end verification is something very unique. CompCert is a great accomplishment, but it is only a medium-sized program, it required a world-expert to write, and even then it tool a lot of effort and still he skimped on the termination proofs.

Imperative tools, OTOH, are used every day by thousands of engineers to write verified software of various kinds (e.g., [1]). So the answer to your question is: except for end-to-end verification, which is extremely costly with any approach, they can do better. In fact, as promising as FP approaches may be, they are still very much in the lab with nearly negligible industry use (and in the one or two cases Coq has been used in the industry, it was always done jointly with academics).

Also, I'm a bit puzzled because you specifically mentioned OCaml, which is an imperative functional language.

In fact, while the difference between programming language in terms of general amenability to formal methods is not great, there are certainly large differences in amenability to model checking. This is why a language like SCADE (based on Esterel and the FRP-ish Lustre) is a fairly widely used tool in aviation software. If anything, a synchronous language like Esterel or the modern Céu[2] are a better choice if you want your verification to be as automatic as possible and run in a resource-constrained environment (that's killing two birds with one stone).

> As far as Europe is concerned, FP does appear to be the future of formal verification.

Even if you look at INRIA, the most European of institutions and the birthplace of Coq, you'll see that they dedicate significant verification research to other approaches[3]. At Max Planck, FP is a clear minority[4].

And if you look at the academic community at large without artificially restricting it to Europe (which certainly has a linguistic bias), you'll see that the verification community is certainly not betting on FP (although they are certainly exploring it). Don't get me wrong: FP and linguistic approaches is certainly one avenue among several showing promise in verification. But it is downright false to say that this approach is recognized as "the future of verification".

[1]: https://verificationinstitute.org/wp-content/uploads/sites/2...

[2]: http://www.ceu-lang.org/

[3]: http://www.inria.fr/en/teams/veridis

[4]: http://plv.mpi-sws.org/

I want to see Etherium work, and it is extremely unfortunate that basically THE first high profile smart contract has gone sideways. But I'm not sure if I want there to be anything we can do about it. The whole point of this project is that the blockchain is supposed to be like an indifferent force of nature.

I wouldn't be so hard on the kid. Now, the due diligence that should have been performed by the corporations that sank millions in to this project, who actually do hire plenty of people who are well educated and should have known better is another matter.

But I suppose jumping in early in to the tulip craze and riding it for all its worth is more important than taking the time and effort to make sure the system is reliable and robust before it goes live.