Wikipedia

F* (programming language): Difference between revisions

Browse history interactively
← Previous edit
Content deleted Content added
VisualWikitext
 
(28 intermediate revisions by 17 users not shown)
Line 1:
{{distinguishShort description|FFunctional (programming language) inspired by ML and aimed at program verification}}
{{distinguish|F (programming language)|F＃ (programming language)}}
{{Infobox programming language
| name = F*
| logo = Fstar-official-logo-2015.png
| logo_size logo size = 128px
| logo caption = The official F* = logo
| paradigm = [[multiMulti-paradigm programming language|Multi-paradigm]]: [[functionalFunctional programming|functional]], [[imperativeImperative programming|imperative]]
| family = [[ML (programming language)|ML]]: [[Caml]]: [[OCaml]]
| latest release version = [https://github.com/FStarLang/FStar repository]
| designers = Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
| latest release date =
| developers = [[Microsoft Research]],<br/>[[French Institute for Research in Computer Science and Automation|Inria]]<ref name="MS-Inria">{{cite web |url=https://www.microsoft.com/en-us/research/collaboration/inria-joint-centre/ |title=Microsoft Research Inria Joint Centre |website=MSR-INRIA}}</ref>
| typing = [[Dependent types|Dependent]], [[type inference|inferred]], [[static typing|static]], [[strong typing|strong]]
| released = {{Start date and age|2011}}
| implementations =
| latest release version = v2025.03.25<ref name="GitHubCode"/>
| dialects =
| latest release date = {{Start date and age|2025|03|26|df=y}}
| influenced by = [[Coq]], [[Dafny (programming language)|Dafny]], [[F Sharp (programming language)|F#]], [[Lean (proof assistant)|Lean]], [[OCaml]], [[Standard ML]]
| typing = [[Dependent types|dependent]], [[Type inference|inferred]], [[Static typing|static]], [[Strong and weak typing|strong]]
| influenced =
| programming language = F*
| operating system = [[Cross-platform =software|Cross-platform]]: [[Linux]], [[macOS]], [[Windows]]
| license = [[Apache License 2.0|Apache 2.0]]
| website = {{urlURL|https://www.fstar-lang.org/}}
| file ext = .fst
| implementations =
| designers = [[Microsoft Research]] and [[Inria]]<ref>{{cite web|url=http://www.msr-inria.fr/|title=Microsoft Research Inria Joint Centre|website=MSR-INRIA}}</ref>
| dialects =
| file_ext = .fst
| influenced by = [[Dafny (programming language)|Dafny]], [[F Sharp (programming language)|F#]], [[Lean (proof assistant)|Lean]], [[OCaml]], [[Coq (software)|Rocq]], [[Standard ML]]
| influenced =
}}
 
'''F*''' (pronounced ''F star'') is a [[High-level programming language|high-level]], [[Comparison of multi-paradigm programming languages|multi-paradigm]], [[Functional programming|functional]] and [[Object-oriented programming|object-oriented]] [[programming language]] inspired by the languages [[ML (programming language)|ML]], [[Caml]], and aimed[[OCaml]], atand intended for [[program verification]]. It is a joint project of [[Microsoft Research]], and the [[French Institute for Research in Computer Science and Automation]] (Inria).<ref name="MS-Inria"/> Its [[type system]] includes [[dependent types]], [[Monad (functional programming)|monadic]] [[sideSide effect (computer science)|effects]], and [[refinement type]]s. 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 [[proofProof assistant|manual proofs]]. For execution, programs written in F* can be translated to [[OCaml]], [[F Sharp (programming language)|F#]], [[C (programming language)|C]], [[WebAssembly]] (via KaRaMeL tool), or [[assembly language]] (via Vale toolchain). Prior F* versions could also be translated to [[JavaScript]].
Programs written in F* can be translated to [[OCaml]], [[F Sharp (programming language)|F#]], and [[C (programming language)|C]] for execution. Previous versions of F* could also be translated to [[JavaScript]].
 
It was introduced in 2011.<ref name="origin-paper">
The latest version of F* is written entirely in a common subset of F* and [[F Sharp (programming language)|F#]], and bootstraps in both [[OCaml]] and [[F Sharp (programming language)|F#]]. It is open source (under the [[Apache License 2.0]]) and is under active development on [[GitHub]].<ref>{{cite web|url=https://github.com/FStarLang/FStar|title=FStarLang/FStar|website=GitHub}}</ref>
{{cite conference
|last1=Swamy |first1=Nikhil
|last2=Chen |first2=Juan
|last3=Fournet |first3=Cédric
|last4=Strub |first4=Pierre-Yves
|last5=Bhargavan |first5=Karthikeyan
|last6=Yang |first6=Jean
|date=September 2011
|title=Secure distributed programming with value-dependent types
|conference=ICFP '11: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming
|volume=46
|issue=9
|pages=266–278
|___location=Tokyo, Japan
|doi=10.1145/2034574.2034811
|publisher=Association for Computing Machinery
|url=https://dl.acm.org/doi/10.1145/2034773.2034811
|access-date=17 April 2023|url-access=subscription
}}</ref><ref>{{cite web |url=https://www.microsoft.com/en-us/research/project/the-f-project/ |title=The F* Project |website=Microsoft |access-date=20 April 2023}}</ref> and is under active development on [[GitHub]].<ref name="GitHubCode">{{cite web |url=https://github.com/FStarLang/FStar |title=FStarLang/FStar |website=GitHub |access-date=18 May 2025}}</ref>
 
==History==
===Versions===
Until version 2022.03.24, F* was written entirely in a common subset of F* and [[F Sharp (programming language)|F#]] and supported bootstrapping in both [[OCaml]] and F#. This was dropped starting in version 2022.04.02.<ref>{{cite web |title=fstar.exe is no longer buildable in F# as a .NET executable #2512 |url=https://github.com/FStarLang/FStar/pull/2512 |website=Github |access-date=17 April 2023}}</ref><ref>{{cite web |title=Consider dropping requirement that F* code has to be valid F# #1737 |url=https://github.com/FStarLang/FStar/issues/1737 |website=Github |access-date=17 April 2023}}</ref>
 
== Overview ==
 
=== Operators ===
F* supports common arithmetic [[Operator (computer programming)|operators]] such as <code>+</code>, <code>-</code>, <code>*</code>, and <code>/</code>. Also, F* supports relational operators like <code><</code>, <code><=</code>, <code>==</code>, <code>!=</code>, <code>></code>, and <code>>=</code>.<ref name=":0">{{Cite book |last=Swamy |first=Nikhil |url=https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf |title=Proof-Oriented Programming in F* |last2=Martínez |first2=Guido |last3=Rastogi |first3=Aseem |date=Jan 14, 2024}}</ref>
 
=== Data types ===
Common primitive [[Primitive data type|data types]] in F* are <code>bool</code>, <code>int</code>, <code>float</code>, <code>char</code>, and <code>unit</code>.<ref name=":0" />
 
==References==
Line 32 ⟶ 65:
===Sources===
* {{cite conference
|last1=Ahman |first1 = Danel
|last2=Hriţcu |first2=Cătălin
| last1 = Ahman
|last3=Maillard |first3=Kenji
| first2 = Cătălin
|last4=Martínez |first4=Guido
| last2 = Hriţcu
|last5=Plotkin |first5=Gordon
| first3 = Kenji
|last6=Protzenko |first6=Jonathan
| last3 = Maillard
|last7=Rastogi |first7=Aseem
| first4 = Guido
|last8=Swamy |first8=Nikhil
| last4 = Martínez
|year=2017
| first5 = Gordon
|title=Dijkstra Monads for Free
| last5 = Plotkin
|url=https://fstar-lang.org/papers/dm4free/
| first6 = Jonathan
|book-title=44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
| last6 = Protzenko
| first7 = Aseem
| last7 = Rastogi
| first8 = Nikhil
| last8 = Swamy
| title = Dijkstra Monads for Free
| url = https://www.fstar-lang.org/papers/dm4free/
| book-title = 44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
| year = 2017
}}
* {{cite conference
|last1=Swamy |first1 = Nikhil
|last2=Hriţcu |first2=Cătălin
| last1 = Swamy
|last3=Keller |first3=Chantal
| first2 = Cătălin
|last4=Rastogi |first4=Aseem
| last2 = Hriţcu
|last5=Delignat-Lavaud |first5=Antoine
| first3 = Chantal
|last6=Forest |first6=Simon
| last3 = Keller
|last7=Bhargavan |first7=Karthikeyan
| first4 = Aseem
|last8=Fournet |first8=Cédric
| last4 = Rastogi
|last9=Strub |first9=Pierre-Yves
| first5 = Antoine
|last10=Kohlweiss |first10=Markulf
| last5 = Delignat-Lavaud
|last11=Zinzindohoue |first11=Jean-Karim
| first6 = Simon
|last12=Zanella-Béguelin |first12=Santiago
| last6 = Forest
|year=2016
| first7 = Karthikeyan
|title=Dependent Types and Multi-Monadic Effects in F*
| last7 = Bhargavan
|url=https://fstar-lang.org/papers/mumon/
| first8 = Cédric
|book-title=43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
| last8 = Fournet
| first9 = Pierre-Yves
| last9 = Strub
| first10 = Markulf
| last10 = Kohlweiss
| first11 = Jean-Karim
| last11 = Zinzindohoue
| first12 = Santiago
| last12 = Zanella-Béguelin
| title = Dependent Types and Multi-Monadic Effects in F*
| url = https://www.fstar-lang.org/papers/mumon/
| book-title = 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
| year = 2016
}}
* Swamy, Nikhil; Martínez, Guido; Rastogi, Aseem (2024). ''[https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf Proof-Orented Programming in F*].''
 
==External links==
*[https://www.{{Official website|fstar-lang.org/ F* Homepage]}}
*{{GitHub|FStarLang}}
*[https://github.com/FStarLang/FStar F* source code on GitHub]
*[https://www.fstar-lang.org/tutorial/ F* tutorial]
 
{{ML programming}}
{{Microsoft FOSS}}
{{Microsoft development tools}}
Line 94 ⟶ 109:
 
{{DEFAULTSORT:F star (programming language)}}
[[Category:High-level programming languages]]
[[Category:Functional languages]]
[[Category:MLOCaml programming language family]]
[[Category:.NET programming languages]]
[[Category:Microsoft programming languages]]
[[Category:Microsoft Research]]
[[Category:Microsoft free software]]
[[Category:Dependently typed languages]]
[[Category:Automated theorem proving]]
[[Category:Programming languages created in 2011]]
[[Category:Proof assistants]]
[[Category:20132011 software]]
[[Category:Cross-platform free software]]
 
[[Category:Software using the Apache license]]
{{prog-lang-stub}}
[[Category:Statically typed programming languages]]
Retrieved from "https://en.wikipedia.org/wiki/F*_(programming_language)"