F*
F* (pronounced F star) is a functional programming language inspired by ML and aimed at program verification. Its type system includes dependent types, monadic effects, and refinement types. This allows expressing precise specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and manual proofs. Programs written in F* can be translated to OCaml, F#, and C for execution. Previous versions of F* could also be translated to JavaScript. The latest version of F* is written entirely in a common subset of F* and F#, and bootstraps in both OCaml and F#. It is open source (under the Apache License 2.0) and is under active development on GitHub.
Relations
A programming language is a formal language comprising a set of instructions that produce various kin...
Software verification is a discipline of software engineering whose goal is to assure that software f...
Edit details Edit relations Attach new author Attach new topic Attach new resource
Resources
The first four parts of this book explain the main features of the language using a variety of exampl...