F* (programming language)
 | |
| Paradigm | Multi-paradigm: functional, imperative |
|---|---|
| Designed by | Microsoft Research and Inria[1] |
| Stable release | |
| Typing discipline | Dependent, inferred, static, strong |
| OS | Linux, macOS, Windows |
| License | Apache License 2.0 |
| Website | www |
| Influenced by | |
| Coq, Dafny, F#, Lean, OCaml, Standard ML | |
F* (pronounced F star) is a functional programming language inspired by ML and aimed at program verification. 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 SMT solving and manual proofs. Programs written in F* can be translated to OCaml, F#, and C for execution. Previous versions of F* could also be translated to JavaScript.
It was introduced in 2011[2][3] and is under active development on GitHub.[4]
History
Versions
Up 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 beginning in version 2022.04.02.[5][6]
References
- ↑ "Microsoft Research Inria Joint Centre". https://www.microsoft.com/en-us/research/collaboration/inria-joint-centre/.
- ↑ 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. 46. Tokyo, Japan: Association for Computing Machinery. pp. 266–278. doi:10.1145/2034574.2034811. https://dl.acm.org/doi/10.1145/2034773.2034811. Retrieved 17 April 2023.
- ↑ "The F* Project". https://www.microsoft.com/en-us/research/project/the-f-project/.
- ↑ "FStarLang/FStar". https://github.com/FStarLang/FStar.
- ↑ "fstar.exe is no longer buildable in F# as a .NET executable #2512". https://github.com/FStarLang/FStar/pull/2512.
- ↑ "Consider dropping requirement that F* code has to be valid F# #1737". https://github.com/FStarLang/FStar/issues/1737.
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". https://www.fstar-lang.org/papers/dm4free/.
- Swamy, Nikhil; Hriţcu, Cătălin; Keller, Chantal; Rastogi, Aseem; Delignat-Lavaud, Antoine; Forest, Simon; Bhargavan, Karthikeyan; Fournet, Cédric et al. (2016). "Dependent Types and Multi-Monadic Effects in F*". https://www.fstar-lang.org/papers/mumon/.
External links
 |  |
