F* (programming language)
Functional programming language inspired by ML and aimed at program verification From Wikipedia, the free encyclopedia
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.
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 | v2023.09.03[2]
/ 3 September 2023 |
| 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 | |
| Coq, Dafny, F#, Lean, OCaml, Standard ML | |
It was introduced in 2011.[3][4] and is under active development on GitHub.[2]
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 primitive data types in F* are bool, int, float, char, and unit.[7]
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
