F*: Tactics, SMT, and metaprogramming

I'll present the incipient tactics engine for F*, a programming language aimed at verification with an SMT backend. In the quest to make both F* proofs faster and more reliable and the language itself more extensible, we provide a way for user programs to manipulate internal compiler structures for breaking down proof obligations or computing new definitions on the fly. I'll describe the design of the engine (somewhat inspired by Lean's), particularities of it related to F*, and give some mid-sized examples of tactics. To put the pedal to the (actual) metal, we reuse F*'s extraction mechanism to *compile* tactic programs and *link* them into the compiler dynamically, obtaining much greater performance.