Yes, in a sense. But the reason they're expensive is they don't work very well and prove only trivial things. Try using any imperative language with integrated

Yes, in a sense. But the reason they're expensive is they don't work very well and prove only trivial things. Try using any imperative language with integrated proof predicates like Dafny, Whiley, etc. You'll immediately notice that they struggle to understand even properties of the code that looks extremely obvious, for instance they require lots of loop annotations. The examples being proven correct all end up being so trivial that you can just as well prove them correct by simply reading and thinking about them. In the functional space things are hardly better. Formal methods in FP has evolved into dependent types research. But dependent types are more or less dependent on functional languages - the flagship is Idris, which is based on Haskell. But Haskell and other pure FP languages have been around for decades. Despite being extensively promoted to students at universities around the world, these languages have not seen wide adoption, so it stands to reason dependent types can't either. And again, the sorts of things being proven tend to be fairly trivial. The way industry is going is pretty clearly small improvements to existing type systems, in particular, implementing value types into managed languages so the costs of using strong types is lower, where otherwise raw/primitive types would be used. And there's a huge focus on tuning and improving generics, flow typing, type inference and other usability improvements. In other words, industry practitioners don't believe lack of proving power is our problem. They believe we aren't using the power of the type (proof) systems we already have, because the usability is too low. The popularity of JavaScript as a server side language would seem to suggest they are right.