[erk__]

Its not like Microsoft does not work on that, they probably have a dozen different formally verified programming languages around at the moment. You already mentioned F*[0], but there is also Checked C[1], VCC[2], koka[3], dafny[4], Project Verona and probably some more that I am missing. The point being that they have clearly evaluated and have used F-Star for parts of the OS already.

[0]: https://www.fstar-lang.org

[1]: https://www.microsoft.com/en-us/research/project/checked-c/

[2]: https://www.microsoft.com/en-us/research/project/vcc-a-verif...

[3]: https://github.com/koka-lang/koka

[4]: https://github.com/dafny-lang/dafny

[5]: https://www.microsoft.com/en-us/research/project/project-ver...