Nikhil Swamy^{1}
Cătălin Hriţcu^{2}
Chantal Keller^{1,3}
Aseem Rastogi^{4}

Antoine Delignat-Lavaud^{2,5}
Simon Forest^{2,5}
Karthikeyan Bhargavan^{2}
Cédric Fournet^{1,3}

Pierre-Yves Strub^{6}
Markulf Kohlweiss^{1}
Jean-Karim Zinzindohoue^{2,5}
Santiago Zanella-Béguelin^{1}

^{1}Microsoft Research
^{2}Inria
^{3}MSR-Inria
^{4}UMD
^{5}ENS Paris
^{6}IMDEA 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.