F* (programming language)

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search
Not to be confused with F (programming language) or F＃ (programming language).
F*
The official F* logo
ParadigmMulti-paradigm: functional, imperative
FamilyML: Caml: OCaml
Designed byNikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
DevelopersMicrosoft Research,
Inria[1]
First appeared2011; 15 years ago (2011)
Stable release
v2025.03.25[2] / 26 March 2025; 13 months ago (2025-03-26)
Typing disciplinedependent, inferred, static, strong
Implementation languageF*
OSCross-platform: Linux, macOS, Windows
LicenseApache 2.0
Filename extensions.fst
Websitefstar-lang.org
Influenced by
Dafny, F#, Lean, OCaml, Rocq, 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.[3][4] and is under active development on GitHub.[2]

History

[edit | edit source]

Versions

[edit | edit source]

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]

Overview

[edit | edit source]

Operators

[edit | edit source]

F* supports common arithmetic operators such as +, -, *, and /. Also, F* supports relational operators like <, <=, ==, !=, >, and >=.[7]

Data types

[edit | edit source]

Common primitive data types in F* are bool, int, float, char, and unit.[7]

References

[edit | edit source]
  1. ^ a b Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
  2. ^ a b Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
  3. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
  4. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
  5. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
  6. ^ Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
  7. ^ a b Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).

Sources

[edit | edit source]
  • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
  • Lua error in Module:Citation/CS1/Configuration at line 2172: attempt to index field '?' (a nil value).
  • Swamy, Nikhil; Martínez, Guido; Rastogi, Aseem (2024). Proof-Oriented Programming in F*.
[edit | edit source]
Retrieved from "http://70.231.62.181/index.php?title=F*_(programming_language)&oldid=12624938"