Tactics and Metaprogramming with Meta-F*

This part of the book is still heavily under construction

So far, we have mostly relied on the SMT solver to do proofs in F*. This works rather well: we got this far, after all! However, sometimes, the SMT solver is really not able to complete our proof, or takes too long to do so, or is not robust (i.e. works or fails due to seemingly insignificant changes).

This is what Meta-F* was originally designed for. It provides the programmer with more control on how to break down a proof and guide the SMT solver towards finding a proof by using tactics. Moreover, a proof can be fully completed within Meta-F* without using the SMT solver at all. This is the usual approach taken in other proof assistants (such as Lean, Coq, or Agda), but it’s not the preferred route in F*: we will use the SMT for the things it can do well, and mostly write tactics to “preprocess” obligations and make them easier for the solver, thus reducing manual effort.

Meta-F* also allows for metaprogramming, i.e. generating programs (or types, or proofs, …) automatically. This should not be surprising to anyone already familiar with proof assistants and the Curry-Howard correspondence. There are however some slight differences between tactic-based proofs and metaprogramming, and more so in F*, so we will first look at automating proofs (i.e. tactics), and then turn to metaprogramming (though we use the generic name “metaprogram” for tactics as well).

In summary, when the SMT solver “just works” we usually do not bother writing tactics, but, if not, we still have the ability to roll up our sleeves and write explicit proofs.

Speaking of rolling up our sleeves, let us do just that, and get our first taste of tactics.