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.