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...

Cool! Can you develop them interactively in Emacs, like in Coq, observing how individual tactics change the proof state?

Sadly not yet. You can see each individual intermediate state but the thing runs fully. We certainly plan to add such a feature though!

We've been mostly studying hammer-like tactics to, say, apply some theorems at specific places in the goal (which the SMT might be bad at), and not for chaining small rewriting or logical steps (which the SMT is good at).

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...