A hacker stole $31M of Ether – how it happened, and what it means for Ethereum

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.

One of the key and powerful features of the Ethereum Virtual Machine or, EVM, is the ability to delegate execution to external libraries. You can think of this much the same way you think of installing 3rd party libraries in your favorite programming language of choice.

In the EVM you can write a "library" which performs some common functionality such as manipulation of date-time objects much like the `datetime` library in Python. Any other contract may then make use of this code simply by delegating execution to the deployed library address. This has inherent risks that every Ethereum developer should understand fully, but with that risk comes some incredible power and potential.

There currently is no "Standard Library" for the EVM but it is looking very likely that it will be comprised of this type of contract. Slowly, overtime, these library contracts will be written and deployed to the network. There is work being done on using theorem solvers to mathematically prove that a contract satisfies certain properties which opens the door to a "provably correct" standard library.

I know of no other computing environment or packaging system that has these properties. For me, it has been an enlightening subject and I feel like we've only just scratched the surface.

I think a good analogy here is to compare to American settlers. You're going to have a few waves: the explorers who move into totally uncharted territory and take on significant risk by using smart contracts. These are kinda crazy people who love the innovation, and I'd argue this is the majority of people in the space right now.

Eventually there will be the settlers, who start finding early uses for this technology that can significantly lower costs. Basically collecting on low-hanging fruit. J.P. Morgan, many finance companies, some savvy governments will step in to capitalize on easy wins.

Then there will be the long tail of normal uses. By the time the average company invests in smart contracts, there will be very well-understood battle-tested templates and toolchains for creating smart contracts, as well as consulting firms that are specialized in writing them for you with provable security guarantees.

Right now it's early. Your average company should not use smart contracts, that's a no-brainer. But someday the economics are going to make it a no-brainer for certain things, like incorporation, or issuing shares, or doing payroll, or complying with import/export regulations, or doing corporate taxes, or whatever it is that ends up more efficient through blockchains.

Also, here's a possibly crazy idea: could one create bug bounties for algorithms (or even arbitrary software) on the Ethereum blockchain by writing the algorithm into a contract such that if you somehow break it you receive the bounty?

An example of this would be the massive implicit bounty currently placed on the crypto algorithms (SHA256, ECDSA/Secp256k1, etc) underpinning cryptocurrencies (of course, if those were broken the value of the cryptocurrency would plummet instantly)