F* (programming language)
Inria[1] | |
| Stable release | |
|---|---|
F* (pronounced F star) is a
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]
Overview
Operators
F* supports common arithmetic operators such as +, -, *, and /. Additionally, F* supports relational operators like <, <=, ==, !=, >, and >=.[7]
Data types
Common primitives data types in F* are bool, int, float, char, and unit.[7]
References
- ^ "Microsoft Research Inria Joint Centre". MSR-INRIA.
- ^ 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. . Retrieved 17 April 2023.
- ^ "The F* Project". Microsoft. Retrieved 20 April 2023.
- ^ "FStarLang/FStar". GitHub. Retrieved 17 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
| Programming tools | |||
|---|---|---|---|
| Theorem provers, proof assistants | |||
| Designers |
|---|
Book 
Category:Family:ML Category:Family:OCaml Category:Software:OCaml| Others | ||
|---|---|---|
- Dynamics AX
- BASIC
- Visual Basic
- Bosque
- Visual C++
- C#
- C/AL
- Dafny
- Dexterity
- F#
- F*
- Visual FoxPro
- Java
- JavaScript
- IronPython
- IronRuby
- Lean
- P
- Power Fx
- PowerShell
- Project Verona
- Q#
- Small Basic
- VPL
- XAML
frameworks
| Native | |
|---|---|
| .NET | |
| Device drivers |
| SQL Server | |
|---|---|
| SQL services | |
| Other |
debugging
| Main projects |
| ||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| MSR Labs applied research |
| ||||||||||||||
 | This programming-language-related article is a stub. You can help Wikipedia by expanding it. |