Home > Software > Development > Language > F* language
Details
- Package ID
- FStar
- Version
- 0.9.6.001
- Downloads
- 1131
- Website
- https://www.fstar-lang.org/
Summary
An ML-like language aimed at program verification
Description
F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, or C code. This enables verifying the functional correctness and security of realistic applications, such as a verified HTTPS stack.
F's type system includes dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact 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 interactive proofs.