> 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?