F* (programming language)

Last updated
F*
Fstar-official-logo-2015.png
Paradigm Multi-paradigm: functional, imperative
Designed by Microsoft Research and Inria [1]
Stable release
Typing discipline Dependent, inferred, static, strong
OS Linux, macOS, Windows
License Apache License 2.0
Website www.fstar-lang.org
Influenced by
Coq, Dafny, F#, Lean, OCaml, Standard ML

F* (pronounced F star) is a functional programming language inspired by ML and aimed at program verification. 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 SMT solving and manual proofs. Programs written in F* can be translated to OCaml, F#, and C for execution. Previous versions of F* could also be translated to JavaScript.

Contents

It was introduced in 2011 [2] [3] and is under active development on GitHub. [4]

History

Versions

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

Related Research Articles

OCaml is a general-purpose, high-level, multi-paradigm programming language which extends the Caml dialect of ML with object-oriented features. OCaml was created in 1996 by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy, Ascánder Suárez, and others.

<span class="mw-page-title-main">Coq (software)</span> Proof assistant

Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.

In computing, an effect system is a formal system that describes the computational effects of computer programs, such as side effects. An effect system can be used to provide a compile-time check of the possible effects of the program.

<span class="mw-page-title-main">Xavier Leroy</span> French computer scientist and programmer (born 1968)

Xavier Leroy is a French computer scientist and programmer. He is best known for his role as a primary developer of the OCaml system. He is Professor of software science at Collège de France. Before his appointment at Collège de France in 2018, he was senior scientist at the French government research institution Inria.

In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists". In functional programming languages like Agda, ATS, Coq, F*, Epigram, Idris, and Lean, dependent types help reduce bugs by enabling the programmer to assign types that further restrain the set of possible implementations.

<span class="mw-page-title-main">Damien Doligez</span> French academic and programmer

Damien Doligez is a French academic and programmer. He is best known for his role as a developer of the OCaml system, especially its garbage collector. He is a research scientist at the French government research institution INRIA.

The join-calculus is a process calculus developed at INRIA. The join-calculus was developed to provide a formal basis for the design of distributed programming languages, and therefore intentionally avoids communications constructs found in other process calculi, such as rendezvous communications, which are difficult to implement in a distributed setting. Despite this limitation, the join-calculus is as expressive as the full π-calculus. Encodings of the π-calculus in the join-calculus, and vice versa, have been demonstrated.

In functional programming, a generalized algebraic data type is a generalization of parametric algebraic data types.

Solidity is a programming language for implementing smart contracts on various blockchain platforms, most notably, Ethereum. Solidity is licensed under GNU General Public License v3.0. Solidity was designed by Gavin Wood and developed by Christian Reitwiessner, Alex Beregszaszi, and several former Ethereum core contributors. Programs in Solidity run on Ethereum Virtual Machine or on compatible virtual machines.

QuickCheck is a software library, specifically a combinator library, originally written in the programming language Haskell, designed to assist in software testing by generating test cases for test suites – an approach known as property testing.

Nix is a cross-platform package manager. It is built with the eponymous "Nix" programming language and employs a model in which software packages are each installed into unique directories. These directory names correspond to cryptographic hashes of the contents of each package. A package's hash takes into account all of its dependencies. This solves the potential issue of installing many packages with differing versions of same shared library dependencies, and is claimed to eliminate so-called dependency hell, As a result, this package management model advertises more reliable, reproducible, and portable packages.

ProVerif is a software tool for automated reasoning about the security properties of cryptographic protocols. The tool has been developed by Bruno Blanchet and others.


Haskell is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research, and industrial applications, Haskell has pioneered a number of programming language features such as type classes, which enable type-safe operator overloading, and monadic input/output (IO). It is named after logician Haskell Curry. Haskell's main implementation is the Glasgow Haskell Compiler (GHC).

Gradual typing is a type system in which some variables and expressions may be given types and the correctness of the typing is checked at compile time and some expressions may be left untyped and eventual type errors are reported at runtime. Gradual typing allows software developers to choose either type paradigm as appropriate, from within a single language. In many cases gradual typing is added to an existing dynamic language, creating a derived language allowing but not requiring static typing to be used. In some cases a language uses gradual typing from the start.

HipHop Virtual Machine (HHVM) is an open-source virtual machine based on just-in-time (JIT) compilation that serves as an execution engine for the Hack programming language. By using the principle of JIT compilation, Hack code is first transformed into intermediate HipHop bytecode (HHBC), which is then dynamically translated into x86-64 machine code, optimized, and natively executed. This contrasts with PHP's usual interpreted execution, in which the Zend Engine transforms PHP source code into opcodes that serve as a form of bytecode, and executes the opcodes directly on the Zend Engine's virtual CPU.

<span class="mw-page-title-main">WebAssembly</span> Cross-platform assembly language and bytecode designed for execution in web browsers

WebAssembly defines a portable binary-code format and a corresponding text format for executable programs as well as software interfaces for facilitating interactions between such programs and their host environment.

<span class="mw-page-title-main">PureScript</span> Strongly-typed language that compiles to JavaScript

PureScript is a strongly-typed, purely-functional programming language that transpiles to JavaScript, C++11, Erlang, and Go. It can be used to develop web applications, server side apps, and also desktop applications with use of Electron or via C++11 and Go compilers with suitable libraries. Its syntax is mostly comparable to that of Haskell. In addition, it introduces row polymorphism and extensible records. Also, contrary to Haskell, the PureScript language is defined as having a strict evaluation strategy, although there are non-conforming back ends which implement a lazy evaluation strategy.

Futhark is a functional data parallel array programming language originally developed at UCPH Department of Computer Science (DIKU) as part of the HIPERFIT project. It focuses on enabling data parallel programs written in a functional style to be executed with high performance on massively parallel hardware, in particular on graphics processing units (GPUs). Futhark is strongly inspired by NESL, and its implementation uses a variant of the flattening transformation, but imposes constraints on how parallelism can be expressed in order to enable more aggressive compiler optimisations. In particular, irregular nested data parallelism is not supported.

<span class="mw-page-title-main">Owl Scientific Computing</span> Numerical programming library for the OCaml programming language

Owl Scientific Computing is a software system for scientific and engineering computing developed in the Department of Computer Science and Technology, University of Cambridge. The System Research Group (SRG) in the department recognises Owl as one of the representative systems developed in SRG in the 2010s. The source code is licensed under the MIT License and can be accessed from the GitHub repository.

In type theory, session types are used to ensure correctness in concurrent programs. They guarantee that messages sent and received between concurrent programs are in the expected order and of the expected type. Session type systems have been adapted for both channel and actor systems.

References

  1. "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. Vol. 46. Tokyo, Japan: Association for Computing Machinery. pp. 266–278. doi:10.1145/2034574.2034811 . Retrieved 17 April 2023.
  3. "The F* Project". Microsoft. Retrieved 20 April 2023.
  4. "FStarLang/FStar". GitHub. Retrieved 17 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.

Sources