Abstract

Fstar (https://fstar-lang.org) is a verification-oriented programming language that follows in the tradition of ML. Like ML, Fstar is a typed, strict, and effectful functional programming language. However, Fstar type system is significantly richer than ML’s, allowing program specifications, including effects, to be stated and checked semi-automatically.

To prove that a program meets its type and effect specification, the Fstar type checker uses a weakest precondition calculus to compute verification conditions, which it then tries to discharge using the Z3 SMT solver. Crucially, there is no distinction between the language used to write programs and specifications. Consistency is maintained by verifying that specifications are pure, terminating computations.

This talk will be organized as a tutorial. I will gradually introduce the features of the language with the help of interactive demos. Some familiarity with functional programming languages, specially Fsharp or ML, can help, but it is not required.

Those willing to learn about advanced features of Fstar, like extraction to OCaml and C, verification of stateful programs using hyper heaps, and our ongoing work on verifying the TLS protocol, are welcome to stay after the first part of the talk.