What stops us is cost. Formally verifying non-trivial properties (in the sense of CompCert) with current technology is several orders of magnitude more expensiv

What stops us is cost. Formally verifying non-trivial properties (in the sense of CompCert) with current technology is several orders of magnitude more expensive and time-consuming than programming and a bit of testing. And this price is almost never worth it. We hope that this cost can be lowered in the future.