> Previously the options were reference counts, garbage collection, or bugs.

I think you mean “lack of memory safety” rather than bugs. Garbage collection doesn't magically free you from finalization bugs, it just makes their consequences less disastrous.

> Formal methods are still a pain. The technology tends to come from people in love with the theory, resulting in systems that are too hard to use.

Clearly, the solution is getting rid of people, but it isn't entirely clear on which end to get rid of people.