F* | |
Logo Size: | 128px |
Logo Caption: | The official Fstar logo |
Paradigm: | Multi-paradigm |
Family: | ML |
Designers: | Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang |
Developers: | Microsoft Research, Inria[1] |
Latest Release Version: | v2023.09.03 |
Typing: | dependent, inferred, static, strong |
Programming Language: | F* |
Operating System: | Cross-platform |
License: | Apache 2.0 |
File Ext: | .fst |
Influenced By: | Coq, Dafny, F#, Lean, OCaml, Standard ML |
F* (pronounced F star) is a high-level, multi-paradigm, functional and object-oriented programming language inspired by the languages ML, Caml, and OCaml, and intended for program verification. It is a joint project of Microsoft Research, and the French Institute for Research in Computer Science and Automation (Inria).[1] 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 satisfiability modulo theories (SMT) solving and manual proofs. For execution, programs written in F* can be translated to OCaml, F#, C, WebAssembly (via KaRaMeL tool), or assembly language (via Vale toolchain). Prior F* versions could also be translated to JavaScript.
It was introduced in 2011.[2] [3] and is under active development on GitHub.[4]
Until version 2022.03.24, F* was written entirely in a common subset of F* and F# and supported bootstrapping in both OCaml and F#. This was dropped starting in version 2022.04.02.[5] [6]
F* supports common arithmetic operators such as +
, -
, *
, and /
. Also, F* supports relational operators like <
, <=
, ==
, !=
, >
, and >=
.[7]
Common primitives data types in F* are bool
, int
, float
, char
, and unit
.