ML originated as the metalanguage for constructing proofs in the LCF theorem prover. Due to its many virtues, it became a rôle model for object-level languages as well, inspiring an entire family of strict functional programming languages.

A member of this family is F*, a verification-oriented dialect of ML including dependent types and a monadic effect system, the combination of which allows to express arbitrarily complex properties of (effectful!) programs within the type system itself. To prove these properties, F* relies on querying an SMT solver (usually Z3). For properties in well-supported SMT theories (e.g. linear arithmetic or uninterpreted functions) this approach works very well, allowing programmers to verify programs with relative ease. However, for poorly-supported theories (e.g. non-linear arithmetic), the SMT solver might require a prohibitive amount of resources or be wildly inpredictable. Furthermore, these rotten apples spoil the barrel, since combining even a basic proveable fact from a poorly-supported theory with a well-supported one might stump the solver.

Motivated by these issues, we have recently extended F* with a tactics engine, which allows to attack proof obligations with user-defined procedures. Tactics are written in Meta-F* , which is simply the set of those F* programs of a particular Tac effect, defined within the existing type-and-effect system. As such, they readily interoperate with the rest of language and can themselves be verified (to a degree). Using tactics allows the programmer to massage proof obligations before querying the SMT solver (possibly simplifying them into the well-supported fragments) or even solving them completely.

Here, we present an overview of the tactics and metaprogramming engine of F*, focusing on the design of the metalanguage and its execution models. In addition, we discuss the benefits of tactics and metaprogramming in F* through some idiomatic case studies.