beurdouche

F* now has tactics, it is very new, but no doubt that it will evolve a lot... https://github.com/FStarLang/FStar/tree/master/examples/tact...

One cool thing with F* is that it starts bringing real contributions such as the HACL* formally verified cryptography to Firefox. https://blog.mozilla.org/security/2017/09/13/verified-crypto... Realistically, even if F* is not fully foundational it seems to be a very good compromise to write security sensitive applications in terms of proof effort...