> Smart people building critical systems do not run to relatively untested languages, no matter how good they may look. Except they do, if the new untested lan

> Smart people building critical systems do not run to relatively untested languages, no matter how good they may look. Except they do, if the new untested language is qualitatively better than the old one. For example, a critical crypto algorithm in Firefox is written in F* and compiled to C: https://blog.mozilla.org/security/2017/09/13/verified-cryptography-firefox-57/ https://blog.mozilla.org/security/2017/09/13/verified-crypto... . The new implementation is formally verified free of certain classes of bugs (like buffer overflows), and significantly faster than the hand-written C implementation.