Nikhil Swamy1
Cătălin Hriţcu2
Chantal Keller1,3
Aseem Rastogi4
Antoine Delignat-Lavaud2,5
Simon Forest2,5
Karthikeyan Bhargavan2
Cédric Fournet1,3
Pierre-Yves Strub6
Markulf Kohlweiss1
Jean-Karim Zinzindohoue2,5
Santiago Zanella-Béguelin1
1Microsoft Research
2Inria
3MSR-Inria
4UMD
5ENS Paris
6IMDEA Software Institute
Symposium on Principles of Programming Languages, POPL 2016
We present a new, completely redesigned, version of F*, a language
that works both as a proof assistant as well as a general-purpose,
verification-oriented, effectful programming language.
In support of these complementary roles, F* is a dependently typed,
higher-order, call-by-value language with primitive effects
including state, exceptions, divergence and IO. Although primitive,
programmers choose the granularity at which to specify effects by
equipping each effect with a monadic, predicate transformer
semantics. F* uses this to efficiently compute weakest preconditions
and discharges the resulting proof obligations using a combination of
SMT solving and manual proofs. Isolated from the effects, the core of
F* is a language of pure functions used to write specifications and
proof terms---its consistency is maintained by a semantic termination
check based on a well-founded order.
We evaluate our design on more than 55,000 lines of F* we have
authored in the last year, focusing on three main case
studies. Showcasing its use as a general-purpose programming language,
F* is programmed (but not verified) in F*, and bootstraps in both
OCaml and F#. Our experience confirms F*'s pay-as-you-go cost model:
writing idiomatic ML-like code with no finer specifications imposes no
user burden. As a verification-oriented language, our most significant
evaluation of F* is in verifying several key modules in an
implementation of the TLS-1.2 protocol standard. For the modules we
considered, we are able to prove more properties, with fewer
annotations using F* than in a prior verified implementation of
TLS-1.2. Finally, as a proof assistant, we discuss our use of F* in
mechanizing the metatheory of a range of lambda calculi, starting from
the simply typed lambda calculus to System F-omega and even micro-F*,
a sizeable fragment of F* itself---these proofs make essential use of
F*'s flexible combination of SMT automation and constructive proofs,
enabling a tactic-free style of programming and proving at a
relatively large scale.