[electronvolt]

> We're not even close to a world where tools can offer amazing protection.

Actually, we're reasonably close--the tools aren't quite there yet for mass consumption (many are still feel quite researchy), but given that the trend of (research -> industry) usually takes 10-25 years, I'd expect that more and more critical systems will be formally verified in 10 years. Even now, companies like Amazon are using some formal methods (modelling with TLA+) to validate that specifications will behave as expected. (https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-...)

Formal methods & dependent types allow for some very cool tricks on top of that--basically, you can encode in the type system a proof that the program implementation matches a specification. CompCert is a mostly-formally verified C compiler--since it was released, iirc, no bugs have been found in the verified portion of the compiler. (CompCert page: http://compcert.inria.fr/man/manual001.html)

You can also prove that the specification has particular properties (in a distributed system, things like liveness and partition tolerance). Consider the Verdi framework (allows formal verification of distributed protocols) and their formal verification of RAFT. (Code here: https://github.com/uwplse/verdi-raft)

However--it's just that it currently takes a lot more work in terms of person-hours to do the development. But formal methods are getting used in more and more places, and they do make a difference in practice. (Wired has a not particularly deep, but straightforward article that shows another use: https://www.wired.com/2016/09/computer-scientists-close-perf... )

Anecdotally, as far as effort--I'm an industry programmer who writes mostly C#. I had to learn Coq (a formally verified language) for a class--it took me a couple of simple assignments to get the idea of how it worked. Even after a few months, hacking together a formally verified interpreter for a very simple language (functions, while loops, etc.--simple, but not trivial) took about 3-4 times longer than it would have taken me to do normally.

[seanwilson]

I think the problem is that the language for smart contracts that backs Ether hasn't been written with formal verification in mind. You could apply formal methods to anything after the fact but it doesn't look like they've made this easy here. You could claim that a C program could be made bug free eventually by applying formal methods for example but it would require a huge amount of work.

Is there a good reason they didn't use a battle tested pure functional language with a strong and expressive type system?

[electronvolt]

I'd agree, and the article basically says the same thing--the language is too expressive, and therefore hard to analyze. I don't know that much about the Ether devs, but I'd expect it just didn't occur to them--even among PL folks, knowledge & experience with something like coq is somewhat rare unless you went to the right undergrad or grad school. Especially if you weren't keeping up with the latest research in the last ~5-10 years or so.

Something like Coq with a few primitives to represent interacting with the Ether network, and an optimizing, verified cross compiler would have been a perfect fit for this sort of thing, in my opinion. It's a shame that they didn't go that route, the extra dev time to get it right probably wouldn't have been equivalent to 200+ dev-years of cost (~31 million).

[seanwilson]

> I don't know that much about the Ether devs, but I'd expect it just didn't occur to them--even among PL folks, knowledge & experience with something like coq is somewhat rare unless you went to the right undergrad or grad school. Especially if you weren't keeping up with the latest research in the last ~5-10 years or so.

Hmm, you'd think they'd know about languages like Haskell though.

I don't think it would be practical to expect developers to write verified code anyway; it's still far too challenging in general. Having a language where you could optionally formally verify the code would have been useful though.

> Something like Coq with a few primitives to represent interacting with the Ether network, and an optimizing, verified cross compiler would have been a perfect fit for this sort of thing, in my opinion

You wouldn't think something like Coq with a few primitives would make some contracts difficult to write?

[electronvolt]

Late response, but: coq has the optional verification that you're proposing. :)

In my experience, Coq is not significantly harder than OCaml to write unverified code in. It's missing some nice shorthand syntax, but other than that it feels pretty similar.

With coq, the main challenge is expressing things that are meant to "run forever" (any truly unbounded recursion)--but my understanding is that would be forced to halt when it ran out of ether (so it's bounded anyways, and if you needed to you could probably explicitly hand that fact to the compiler)--and I think you probably don't want something to loop indefinitely if each iteration costs ether.

The main issues with coq that I think you'd crop up against are things that a good optimizer/compiler could probably help with (e.x. things like the fact that integers are naively represented as cons cells, so addition is O(n) and multiplication is worse). However, I haven't written any smart contracts, so it's definitely possible I'm missing something obvious.