F* (programming language): Difference between revisions

Revision as of 09:35, 12 May 2024

Latest revision as of 11:24, 5 July 2025

(11 intermediate revisions by 8 users not shown)

Line 5:

| logo = Fstar-official-logo-2015.png

| logo size = 128px

| logo caption = The official FstarF* logo

| paradigm = [[Multi-paradigm programming language|Multi-paradigm]]: [[Functional programming|functional]], [[Imperative programming|imperative]]

| family = [[ML (programming language)|ML]]: [[Caml]]: [[OCaml]]

Line 11:

| 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>

| released = {{Start date and age|2011}}

| latest release version = v2023.09v2025.03.25<ref name="GitHubCode"/>

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

| typing = [[Dependent types|dependent]], [[Type inference|inferred]], [[Static typing|static]], [[Strong and weak typing|strong]]

| programming language = F*

| operating system = [[Cross-platform software|Cross-platform]]: [[Linux]], [[macOS]], [[Windows]]

| license = [[Apache License 2.0|Apache 2.0]]

| website = {{URL|www.fstar-lang.org}}

| file ext = .fst

| implementations =

| dialects =

| influenced by = [[Coq (software)|Coq]], [[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 [[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).<ref name="MS-Inria"/> Its [[type system]] includes [[dependent types]], [[Monad (functional programming)|monadic]] [[Side 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 [[Proof 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]].

It was introduced in 2011.<ref name="origin-paper">

Line 45:

|publisher=Association for Computing Machinery

|url=https://dl.acm.org/doi/10.1145/2034773.2034811

|access-date=17 April 2023|url-access=subscription

|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=2318 AprilMay 20242025}}</ref>

==History==

Line 54 ⟶ 55:

=== 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://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 ===

Common primitivesprimitive [[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 74 ⟶ 75:

|year=2017

|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

}}

Line 92 ⟶ 93:

|year=2016

|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

}}

* 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*].''

==External links==

*{{Official website|www.fstar-lang.org}}

*{{GitHub|FStarLang}}

*[https://www.fstar-lang.org/tutorial/ F* tutorial]

{{ML programming}}

Line 122 ⟶ 123:

[[Category:Cross-platform free software]]

[[Category:Software using the Apache license]]

[[Category:Statically typed programming languages]]

{{Prog-lang-stub}}