I think we're a year or two away from the same argument being used by languages which enforce proof of correctness. The economics seem to be shifting in that direction.

Finding exploits is getting exponentially cheaper, and the cost of producing proofs is rapidly going down. For a lot of software correctness is rapidly becoming non-optional.