> P got its start in Microsoft software development when it was used to ship the USB 3.0 drivers in Windows 8.1 and Windows Phone
It looks like Microsoft’s does the translation, so the only risk is bugs in the code generator, which seems nice.
There’s also Google’s wuffs, but I don’t think that is formal, it just ensures memory safety.
What it does not mean is that the program is bug free. That would, of course, violate the halting problem, or its generalization Rice's Theorem - non-trivial programs can not have arbitrary properties proven about them.
There's also Gödel's Incompleteness Theorem, obviously, as well as the fact that a proof is only as good as its model.
Even formal verification can be insufficient.
funny enough, much like rust, one of its most widely-deployed applications lives in firefox; see project-everest.github.io
All automagic, can’t see how it could get much simpler than that.
I guess there would be a new build step, that runs when code is checked in, to not burden everyone with all the new toolchain (F*, z3, karamel, maybe OCaml and more). While the generated C code can be read and understood by C programmers, changes to that part should be done in Low* and that may require changes to proofs in F* or to the extraction tool (karamel). That's a pretty big investment for a project like linux and I guess, any work in that direction will happen on forks for a while, before there is enough confidence that such changes are sustainable.
A good first candidate may be HACL* (https://hacl-star.github.io), a cryptographic library that is already used in several projects.