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.
|ML 2018 Meta-F* paper (paper.pdf)||342KiB|
Conference DayFri 28 SepDisplayed time zone: Guadalajara, Mexico City, Monterrey change
13:30 - 15:10
|ML as a Tactic Language, Again|
Guido MartínezCIFASIS-CONICET, Argentina, Danel AhmanUniversity of Ljubljana, Victor Dumitrescu, Nick GiannarakisPrinceton University, Chris HawblitzelMicrosoft Research, Cătălin HriţcuInria Paris, Monal Narasimhamurthy, Zoe ParaskevopoulouPrinceton University, Clément Pit-ClaudelMIT CSAIL, Jonathan ProtzenkoMicrosoft Research, Redmond, Tahina RamananandroMicrosoft Research, n.n., Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft ResearchFile Attached
|Design and verification of functional proof checkers|
|Generic Programming with Combinators and Objects|