F* (programming language) explained

F*
Logo Size:128px
Logo Caption:The official Fstar logo
Paradigm:Multi-paradigm

functional, imperative

Family:ML

Caml: OCaml

Designers:Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
Developers:Microsoft Research,
Inria[1]
Latest Release Version:v2023.09.03
Typing:dependent, inferred, static, strong
Programming Language:F*
Operating System:Cross-platform

Linux, macOS, Windows

License:Apache 2.0
File Ext:.fst
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.[2] [3] and is under active development on GitHub.[4]

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.

References

Sources

External links

Notes and References

  1. Web site: Microsoft Research Inria Joint Centre . MSR-INRIA.
  2. 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. 46. 9. 266–278. Tokyo, Japan. 10.1145/2034574.2034811. Association for Computing Machinery. 17 April 2023.
  3. Web site: The F* Project . Microsoft . 20 April 2023.
  4. Web site: FStarLang/FStar . GitHub . 23 April 2024.
  5. Web site: fstar.exe is no longer buildable in F# as a .NET executable #2512 . Github . 17 April 2023.
  6. Web site: Consider dropping requirement that F* code has to be valid F# #1737 . Github . 17 April 2023.
  7. Book: Swamy, Nikhil . Proof-Oriented Programming in F* . Martínez . Guido . Rastogi . Aseem . Jan 14, 2024.