F* (programming language): Difference between revisions

Revision as of 22:28, 14 April 2024

Revision as of 11:47, 23 April 2024

Line 2:

{{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 Fstar = 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 = v2023.09.03<ref name="GitHubCode"/>

| dialects =

| latest release date = {{Start date and age|2023|09|03|df=y}}

| influenced by = [[Coq (software)|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=https://www.microsoft.com/en-us/research/collaboration/inria-joint-centre/|title=Microsoft Research Inria Joint Centre|website=MSR-INRIA}}</ref>

| dialects =

| file_ext = .fst

| influenced by = [[Coq (software)|Coq]], [[Dafny (programming language)|Dafny]], [[F Sharp (programming language)|F#]], [[Lean (proof assistant)|Lean]], [[OCaml]], [[Standard ML]]

| influenced =

}}

'''F*''' (pronounced ''F star'') is a [[Functional programming|functional]] [[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">

{{cite conference

|last1=Swamy |first1=Nikhil

|last2=Chen |first2=Juan

|first1=Nikhil

|last3=Fournet |first3=Cédric

|last2=Chen

|last4=Strub |first4=Pierre-Yves

|first2=Juan

|last5=Bhargavan |first5=Karthikeyan

|last3=Fournet

|last6=Yang |first6=Jean

|first3=Cédric

|date=September 2011

|last4=Strub

|first4=Pierre-Yves

|last5=Bhargavan

|first5=Karthikeyan

|last6=Yang

|first6=Jean

|title=Secure distributed programming with value-dependent types

|conference=ICFP '11: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming

|volume=46

|date=September 2011

|issue=9

|volume=46

|pages=266–278

|issue=9

|___location=Tokyo, Japan

|pages=266–278

|doi=10.1145/2034574.2034811

|___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}}</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=1723 April 2023 2024}}</ref>

==History==

===Versions===

Up untilUntil 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 Sharp (programming language)|F#]]. This was dropped beginningstarting 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>. AdditionallyAlso, 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://www.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 ===

Line 69 ⟶ 64:

===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://www.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://www.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://www.fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf Proof-Orented Programming in F*].''