There is a small community of people interested in formal verification. Unfortunately, it is mostly confined to the academic and research communities, rather than regular software engineers. In part because the tools they use do not have the same level of productivity.

But it seems like one possible next step in programming language evolution. Security and correctness will likely matter more and more.

Productively producing incorrect and insecure code may be less valuable in an age where machine learning and botnets are constantly improving and trying to break into your systems, and where a greater and greater percentage of GDP is dependent upon systems not failing. Increasingly we are building systems where lives are on the line, and failure is not an option.

I would say that this does kind of end up as a bit of an aesthetic divide. Because this is kind of an old school view. There's whole aspects of computing right now that are very trendy which have thrown that old school approach out the window.

The field of machine learning is fine with having systems where they have no real idea of what a system will do, whether that result will for sure be correct, how it came up with a particular result, or reliably being able to reproduce the same result with the same inputs.

They may recognize that those are deficiencies, and be working to improve that, but ultimately their paradigm is inductive and statistical, and thus error-prone by its very nature. They recognize that this is a valuable tradeoff for many applications, and a way to build systems that do interesting things right now.

The "symbolic" AI approach would likely take decades to make visible progress.