The main reason is formal method is still not cost-efficient, not even close. The problem is similar to statically typed languages. Of course, having a sound t

The main reason is formal method is still not cost-efficient, not even close. The problem is similar to statically typed languages. Of course, having a sound type system can help you avoid a lot of stupid mistakes. But the key point of modern statically typed language does not lose a lot of velocities. Sometimes even faster because there are better IDEs out there for auto-completion, importing, and much other stuff. I switched from JavaScript to TypeScript only to find I'm faster to write code without losing anything. Before we make formal method widely accepted by the industry, we probably need depdent type languages first. An excellent example is Idris. https://www.idris-lang.org/ https://www.idris-lang.org/ It's a dependent type language, and it can also apply formal method to prove theorems. With its IDE, it is more like pair programming with the type system, it can really fill up a lot of code according to type. This kind of system could have huge potential to be much more powerful than say, IntelliJ IDEA with Java etc. After then you could write code very faster, you could optionally write some proof for the core domain of your system if you like.