Pronounced F Star, F* is a general-purpose functional programming language aimed at program verification.
A joint project between Microsoft Research, Inria, and the F* development community, F* was influenced by Coq, Dafny, F#, OCaml, and Standard ML, F* is available as open-source under the Apache License, and is in active development by the F* community on GitHub.
The language combines the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. Verified programs can be extracted to OCaml, F#, C, WASM, or ASM code for execution. While previous versions could also be translated to JavaScript, that function is no longer available.
The language's type system includes dependent types, monadic effects, refinement types, and a weakest precondition calculus, which together allow for the expression of precise and compact specifications for programs. Its type-checker is designed to prove that programs meet their specifications using a combination of SMT solving and interactive proofs.
The current version of the programming language is written entirely in F*, and bootstraps via OCaml.
The focus of this part of our guide is on the programming language known as F*. Topics related to the language itself, to any variants or close implementations of the language, or to any editors, IDEs, or tools created to facilitate programming in F* are appropriate for this category, along with any F* user groups, forums, guides, or tutorials.
Recommended Resources
F* is a functional programming language inspired by ML and designed by Microsoft Research and the French Institute for Research in Computer Science and Automation, also known as Inria, and currently under active development on GitHub. Distributed under the Apache 2.0 License, binary packages are available as a free download for Windows, macOS, and Linux. Video and text tutorials are presented, a support wiki offers further information, the development team is acknowledged.
https://www.fstar-lang.org/
GitHub, a well-known development platform, hosts the F* development community. Star, a proof-oriented programming language, and KaRaMeL, a tool for extracting low-level F* programs to readable C code, are pinned, and the repositories of other F* files include Emacs support for F*, syntax highlighting for F* in Atom Editor, binary builds of F* and compatible versions of Z3, an F* interactive mode for the Atom editor, a Vim mode for Star, and third-party editors. People profiles are included.
https://github.com/FStarLang/
Proof-Oriented Programming in F*
Provided on the F* development community website, the online tutorial is structured in four parts, explaining the main features of the programming language using a variety of examples, which are designed to be read sequentially, while following along with provided code samples and exercises. Arranged in increasing order of complexity, readers can stop after any of them and have a working knowledge of the language. Included is an online interface where code can be edited and verified.
http://www.fstar-lang.org/tutorial/
Hosted on Zulip, a team chat application, the F* discussion group requires sign-up and login for participation, although anyone is allowed to read posted messages. A brief description of the programming language is provided, with links to other online resources. Streams and topics are listed chronologically, with recent discussions listed first. Topics include the F* programming language, although related topics may also be included. Documentation on using the application is included.
https://fstar.zulipchat.com/
