Authors: Guido Martínez; Danel Ahman; Dumitrescu, Victor; Giannarakis, Nick.
Resumen: ML originated as the metalanguage for constructing proofs in the LCF theorem prover. Due to its manyvirtues, it became a rôle model for object-level languages as well, inspiring an entire family of strict functionalprogramming languages.A member of this family is F⋆, a verification-oriented dialect of ML including dependent types and amonadic effect system, the combination of which allows to express arbitrarily complex properties of (effectful!)programs within its type system itself. To prove these properties, F⋆ relies on querying an SMT solver (usuallyZ3). For properties in well-supported SMT theories (e.g. linear arithmetic or uninterpreted functions) thisapproach works very well, allowing programmers to verify programs with relative ease. However, for poorlysupported theories (e.g. non-linear arithmetic), the SMT solver might require a prohibitive amount of resourcesor be wildly inpredictable. Furthermore, these rotten apples spoil the barrel, since combining even a basicproveable 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 and metaprogramming engine, whichallows to attack proof obligations with user-defined procedures. Tactics are written in Meta-F⋆, which issimply the set of those F⋆ programs of a particular Tac effect, defined within the existing type-and-effectsystem. 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 (possiblysimplifying them into the well-supported fragments) or even solving them completely.Here, we present an overview of Meta-F⋆, focusing on its design and its execution models. In addition, wediscuss the benefits of tactics and metaprogramming in F⋆ through some idiomatic case studies.
Meeting type: Workshop.
Production: ML as a Tactic Language, Again.
Scientific meeting: ML Workshop 2018.
Meeting place: St. Louis, MO.
Organizing Institution: ACM-SIGPLAN.
It's published?: No
Meeting month: 9