Nothing
Aseem Rastogi, Chantal Keller, Simon Forest, Karthik Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Jean-Karim Zinzindohoue, Markulf Kohlweiss, Pierre-Yves Strub
Higher order, effectful, call-by-value
F + dependent types + effects
Highly customizable
Many semi-automated verifiers for first-order languages
Many interactive proof assistants
F* tries to span the divide
Every expression is classified with a indexed, monadic effect
Unconditionally pure:
1 + 1 : Tot int
Conditionally pure:
factorial x : Pure int (requires (x >= 0)) (ensures (fun y -> y >= 0))
By refinement subtyping:
type nat = x:int{x >= 0}
factorial 1 : Tot nat
Stateful:
x := 17 : ST unit (requires (fun h -> h contains x))
(ensures (fun h0 _ h1 -> h1 = upd h0 x 17))
For example:
Can also pick other effects (e.g., Ghost, IO, NonDet, …)
Each effect is a monad equipped with its own WP calculus
Lifting from one effect to another is a monad morphism, embedding one WP calculus in another
x:t -> M s phi_1 ... phi_n
x1:t1 -> ... -> xn:tn -> t
=
x1:t1 -> Tot ( ... -> Tot (xn:tn -> ML t))
fstar factorial.fst
Verified module: Factorial
All verification conditions discharged successfully
The program has type , given the validity of a logical formula
is passed to Z3 to check for validity in context
If the check succeeds, then, from the metatheory of F*, the program is safe at type
Compile to Ocaml or F# for execution
About 45,000 lines of verified code in our test suite.
F* as a proof assistant
F* as a host for several verification-oriented embedded DSLs
F* for verifying cryptographic protocols
How to use F* with F# and OCaml
Demo: Several small verified programs
No objects
No functors; but, F* is like F, so encode if you must
list int
(or list<int>
for F# users)
Just check effects (Pure, Div, ST, Exn, etc. )
Add simple data refinements to check basic invariants
Specify more invariants, towards functional correctness
Relational proofs for optimizations and security properties
Erasure of ghost code and proof terms; erasure of fancy types
Insertion of Obj.magic
… as little as possible
val sort_with: a:Type -> f:total_order a -> l:list a
-> Tot (m:list a{sorted f m /\ permutation l m})
Extraction to and interop with F#
No Obj.t
; only System.Object
list<t>
to list<Object>
No Obj.magic
; only checked casts