My main comment addresses some of this. I think the consensus on this is that most software will use other techniques with lower barrier to entry that leverage stuff built with higher assurance. For example, certain imperative (Ada) and functional (Ocaml) seem to prevent all kinds of errors with decent performance. The Middle Way is to make the toolchain and critical libraries high assurance while the developer uses the basic features of the language with a decent software process. The process aims for good requirements, conservative design, reuse of proven implementation strategies, and good coding styles. These get checked, analyzed, and turned into machine code by trustworthy components.

Such an approach knocks out the vast majority of problems. The rest get squeezed out incrementally over time as research and development continues.