F* (programming language)

F*
	The official Fstar 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
First appeared	2011
Stable release	v2023.09.03 / 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	www.fstar-lang.org
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.^[3]^[4] and is under active development on GitHub.^[2]

^ ^a ^b "Microsoft Research Inria Joint Centre". MSR-INRIA.
^ ^a ^b "FStarLang/FStar". GitHub. Retrieved 23 April 2024.
^ Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean (September 2011). Secure distributed programming with value-dependent types. ICFP '11: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming. Vol. 46. Tokyo, Japan: Association for Computing Machinery. pp. 266–278. doi:10.1145/2034574.2034811. Retrieved 17 April 2023.
^ "The F* Project". Microsoft. Retrieved 20 April 2023.