Misplaced Pages

F* (programming language)

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
(Redirected from F*) Functional programming language inspired by ML and aimed at program verification Not to be confused with F (programming language) or F＃ (programming language).
F*
The official F* 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
First appeared2011; 14 years ago (2011)
Stable releasev2023.09.03 / 3 September 2023; 15 months ago (2023-09-03)
Typing disciplinedependent, inferred, static, strong
Implementation languageF*
OSCross-platform: Linux, macOS, Windows
LicenseApache 2.0
Filename extensions.fst
Websitefstar-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). 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. and is under active development on GitHub.

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.

Overview

Operators

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

Data types

Common primitive data types in F* are bool, int, float, char, and unit.

References

  1. ^ "Microsoft Research Inria Joint Centre". MSR-INRIA.
  2. ^ "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. ^ 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

ML programming
Software
Implementations,
dialects
Caml
Standard ML
Dependent ML
Programming tools
  • Alt-Ergo°
  • Astrée
  • Camlp4°
  • FFTW°
  • Frama-C°
  • Haxe°
  • Marionnet°
  • MTASC°
  • Poplog°
  • Semgrep°
  • SLAM project
    • 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
    • Microsoft free and open-source software (FOSS)
    Overview
    Software
    Applications
    Video games
    Programming
    languages
    Frameworks,
    development tools
    Operating systems
    Other
    Licenses
    Forges
    Related
    Category
    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
    Microsoft Research (MSR)
    Main
    projects
    Languages, compilers
    Distributed–grid computing
    Internet, networking
    Other projects
    Operating systems
    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 Misplaced Pages by expanding it.

    Categories: