F* (programming language)

F* is a High-level [programming language|high-level], multi-paradigm programming languages|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]. Its type system includes dependent types, monadic Side [effect (computer science)|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] solving and manual proofs. For execution, programs written in F* can be translated to OCaml, F#, C, WebAssembly, or assembly language. Prior F* versions could also be translated to JavaScript.
It was introduced in 2011 and is under active development on GitHub.

History

Versions

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.

Overview

Operators

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

Data types

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