F* (programming language): Difference between revisions

Revision as of 20:58, 19 June 2025

Revision as of 05:25, 24 June 2025

Line 1:

{{Short description|Functional 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 = 128px

| logo caption = The official F* logo

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

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

| designers = Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang

| 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 = v2025.03.25<ref name="GitHubCode"/>

| latest release date = {{Start date and age|2025|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|fstar-lang.org}}

| file ext = .fst

| implementations =

| dialects =

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

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