F* (programming language)
Functional programming language inspired by ML and aimed at program verification
From Wikipedia, the free encyclopedia
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.
| F* | |
|---|---|
The official F* logo | |
| Paradigm | Multi-paradigm: functional, imperative |
| Family | ML: Caml: OCaml |
| Designed by | Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang |
| Developers | Microsoft Research, Inria[1] |
| First appeared | 2011 |
| Stable release | v2025.03.25[2]
/ 26 March 2025 |
| Typing discipline | dependent, inferred, static, strong |
| Implementation language | F* |
| OS | Cross-platform: Linux, macOS, Windows |
| License | Apache 2.0 |
| Filename extensions | .fst |
| Website | fstar-lang |
| Influenced by | |
| Dafny, F#, Lean, OCaml, Rocq, Standard ML | |
It was introduced in 2011[3][4] and is under active development on GitHub.[2]
History
Overview
Operators
F* supports common arithmetic operators such as +, -, *, and /. Also, F* supports relational operators like <, <=, ==, !=, >, and >=.[7]
Data types
Common primitive data types in F* are bool, int, float, char, and unit.[7]