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 men

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 https://www.fstar-lang.org [1]: https://www.microsoft.com/en-us/research/project/checked-c/ https://www.microsoft.com/en-us/research/project/checked-c/ [2]: https://www.microsoft.com/en-us/research/project/vcc-a-verifier-for-concurrent-c/ https://www.microsoft.com/en-us/research/project/vcc-a-verif... [3]: https://github.com/koka-lang/koka https://github.com/koka-lang/koka [4]: https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny [5]: https://www.microsoft.com/en-us/research/project/project-verona/ https://www.microsoft.com/en-us/research/project/project-ver...