I think rigorous application of formal methods plus deployment techniques like unikernels have the potential to improve the quality of a lot of software.
I'm more of a pessimist. If you can't get C programmers to handle memory buffers correctly, how are you going to get them to use actual formal methods or annotations that rely on understanding substantially more math than the average programmer has?
Make the infrastructure you run things on provide what appears to be formal methods for interactions, but also make it appear inconsistent over a given regular timeframe. Abusers of the system will find lots of issues with it because it will break unpredictably at random times if they are hammering away. Happy users of the system will having it break every now and again, but will likely avoid making things overly complex as a result of it increasing the chances it will break over a given time period.
Expecting infrastructure to be completely reliable is a fallacy and should be embraced instead of chased.
Suffering on the part of the former "programmer" (hacker) will be paid while obtaining results of various runs to exploit the system from the outside (external). Suffering on the part of the later "programmer" (coder) will be paid internally while working on more efficient solutions.
We'll need to code up the two types of suffering into stores of value, and tie them to cryptocurrencies, but that should be fairly straightforward to implement.
People learned 4GL's, BASIC, Scratch, COBOL, etc pretty easy. That means the solution is make it higher-level with the compiler, type system, protocol generators, etc doing most of the work. They just need a set of tools that let them express themselves in a way constrained enough to let the tooling produce correct code. Eiffel and Ada/SPARK results are also very promising on systematically eliminating errors from large applications. Experienced users will be able to do more than the basic 4GL or whatever.
