F* (programming language)
![]() 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[1] |
First appeared | 2011; 13 years ago (2011) |
Stable release | v2023.09.03[2] / 3 September 2023; 11 months ago (2023-09-03) |
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 |
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
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.[5][6]
Overview
Operators
F* supports common arithmetic operators such as +
, -
, *
, and /
. Also, F* supports relational operators like <
, <=
, ==
, !=
, >
, and >=
.[7]
Data types
Common primitives data types in F* are bool
, int
, float
, char
, and unit
.[7]
References
- ^ 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.
- ^ "fstar.exe is no longer buildable in F# as a .NET executable #2512". Github. Retrieved 17 April 2023.
- ^ "Consider dropping requirement that F* code has to be valid F# #1737". Github. Retrieved 17 April 2023.
- ^ a b Swamy, Nikhil; Martínez, Guido; Rastogi, Aseem (Jan 14, 2024). Proof-Oriented Programming in F* (PDF).
Sources
- Ahman, Danel; Hriţcu, Cătălin; Maillard, Kenji; Martínez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil (2017). "Dijkstra Monads for Free". 44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
- Swamy, Nikhil; Hriţcu, Cătălin; Keller, Chantal; Rastogi, Aseem; Delignat-Lavaud, Antoine; Forest, Simon; Bhargavan, Karthikeyan; Fournet, Cédric; Strub, Pierre-Yves; Kohlweiss, Markulf; Zinzindohoue, Jean-Karim; Zanella-Béguelin, Santiago (2016). "Dependent Types and Multi-Monadic Effects in F*". 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages.
- Swamy, Nikhil; Martínez, Guido; Rastogi, Aseem (2024). Proof-Orented Programming in F*.
External links
- Official website
- FStarLang on GitHub
- F* tutorial
- v
- t
- e
Implementations, dialects |
| ||||||
---|---|---|---|---|---|---|---|
Programming tools | |||||||
Theorem provers, proof assistants |
|
![](http://upload.wikimedia.org/wikipedia/commons/thumb/f/ff/OCaml_Logo.svg/110px-OCaml_Logo.svg.png)
Designers |
---|
- Thierry Coquand
- Steven G. Johnson
- Christine Paulin-Mohring
- Frank Pfenning
- Simon Thompson
![](http://upload.wikimedia.org/wikipedia/commons/thumb/8/89/Symbol_book_class2.svg/16px-Symbol_book_class2.svg.png)
![](http://upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/16px-Symbol_category_class.svg.png)
![](http://upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/16px-Symbol_category_class.svg.png)
![](http://upload.wikimedia.org/wikipedia/en/thumb/9/96/Symbol_category_class.svg/16px-Symbol_category_class.svg.png)
![]() | This programming-language-related article is a stub. You can help Wikipedia by expanding it. |
- v
- t
- e