We present (new) F*, a dependently typed language for writing
general-purpose programs with effects, specifying them within its
functional core, and verifying them semi-automatically, by a
combination of type inference, SMT solving, and manual proofs.
A central difficulty is to ensure the consistency of a core language of proofs within a larger language in which programs may exhibit effects such as state, exceptions, non-termination, IO, concurrency, etc. Prior attempts at solving this problem generally resort to a range of ad hoc methods. Instead, the main novelty of F* is to safely embrace and extend the familiar style of type-and-effect systems with fully dependent types.
F* is founded on a λ-calculus with a range of primitive effects and a dependent type system parameterized by a user-defined lattice of Dijkstra monads. For each monad, the user provides a predicate-transformer that captures its effective semantics. At the bottom of the lattice is a distinguished Pure monad, such that computations typeable as Pure are normalizing---our termination argument is based on well-founded relations and is fully semantic.
We illustrate our design on a series of challenging programming examples. We outline its metatheory on a core calculus, for which we prove soundness and termination of the Pure fragment. We also discuss selected aspects of its fresh typechecker. The F* system is open source; it fully supports our new design; it generates F# and OCaml code; and it bootstraps to several platforms.