F* (programming language)

Functional programming language inspired by ML and aimed at program verification
F*
The official Fstar logo
ParadigmMulti-paradigm: functional, imperative
FamilyML: Caml: OCaml
Designed byNikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
DevelopersMicrosoft Research,
Inria[1]
First appeared2011; 13 years ago (2011)
Stable release
v2023.09.03[2] / 3 September 2023; 8 months ago (2023-09-03)
Typing disciplinedependent, inferred, static, strong
Implementation languageF*
OSCross-platform: Linux, macOS, Windows
LicenseApache 2.0
Filename extensions.fst
Websitewww.fstar-lang.org
Influenced by
Coq, Dafny, F#, Lean, OCaml, Standard ML

F* (pronounced F star) is a high-level, multi-paradigm, functional and object-oriented programming language inspired by the languages 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).[1] Its type system includes 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 satisfiability modulo theories (SMT) solving and manual proofs. For execution, programs written in F* can be translated to OCaml, F#, 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.[3][4] and is under active development on GitHub.[2]

History

Versions

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 starting in version 2022.04.02.[5][6]

Overview

Operators

F* supports common arithmetic operators such as +, -, *, and /. Also, F* supports relational operators like <, <=, ==, !=, >, and >=.[7]

Data types

Common primitives data types in F* are bool, int, float, char, and unit.[7]

References

  1. ^ a b "Microsoft Research Inria Joint Centre". MSR-INRIA.
  2. ^ a b "FStarLang/FStar". GitHub. Retrieved 23 April 2024.
  3. ^ 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. doi:10.1145/2034574.2034811. Retrieved 17 April 2023.
  4. ^ "The F* Project". Microsoft. Retrieved 20 April 2023.
  5. ^ "fstar.exe is no longer buildable in F# as a .NET executable #2512". Github. Retrieved 17 April 2023.
  6. ^ "Consider dropping requirement that F* code has to be valid F# #1737". Github. Retrieved 17 April 2023.
  7. ^ 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

  • Official website
  • FStarLang on GitHub
  • F* tutorial
  • v
  • t
  • e
ML programming
Software
Implementations,
dialects
Caml
Standard ML
Dependent ML
  • ATS°
Programming tools
Theorem provers,
proof assistants
Community
Designers
  • Lennart Augustsson (Lazy ML)
  • Damien Doligez (OCaml)
  • Gérard Huet (Caml)
  • Xavier Leroy (Caml, OCaml)
  • Robin Milner (ML)
  • Don Sannella (Extended ML)
  • Don Syme (F#)
  • Italics = discontinued
  • ° = Open-source software
    Book Category:Family:ML Category:Family:OCaml Category:Software:OCaml
    • v
    • t
    • e
    Overview
    Software
    Applications
    Video games
    • Allegiance
    Programming
    languages
    Frameworks,
    development tools
    Operating systems
    Other
    Licenses
    Forges
    Related
    Category
    • v
    • t
    • e
    Microsoft development tools
    Development
    environments
    Visual Studio
    Others
    Languages
    APIs and
    frameworks
    Native
    .NET
    Device drivers
    Database
    SQL Server
    SQL services
    Other
    Source control
    Testing and
    debugging
    Delivery
    Category
    • v
    • t
    • e
    Main
    projects
    Languages, compilers
    Distributed–grid computing
    Internet, networking
    Other projects
    Operating systems
    • Barrelfish
    • HomeOS
    • Midori
    • Singularity
    • Verve
    APIs
    Launched as products
    MSR Labs
    applied
    research
    Live Labs
    Current
    Discontinued
    FUSE Labs
    Other labs
    Category


    Stub icon

    This programming-language-related article is a stub. You can help Wikipedia by expanding it.

    • v
    • t
    • e