F* - Programming language

F* is an open source programming language created in 2014.

#125on PLDB

10Years Old

250Repos

Download source code:

git clone https://github.com/FStarLang/FStar

Homepage · Source Code · Wikipedia · Docs

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. Read more on Wikipedia...

Tags: programming language
F* is developed on GitHub and has 2,659 stars
There are at least 250 F* repos on GitHub
Early development of F* happened in Microsoft
F* is written in OCaml, Make, Bourne shell, Markdown, F#, Python, C, Dockerfile, JSON, XML, Assembly language, Nix, YAML, Bash, Clojure, Coq, SVG, Haskell, CSV, Lisp
The Google BigQuery Public Dataset GitHub snapshot shows 28 users using F* in 31 repos on GitHub
Pygments supports syntax highlighting for F*
GitHub supports syntax highlighting for F*
fstar-lang.org was registered in 2014
See also: (7 related languages) Linux, F#, OCaml, Standard ML, ML, C, JavaScript
2 PLDB concepts link to F*: Low*, Vale

Example from hello-world:

module Hello

let main = FStar.IO.print_string "Hello World\n"

F* Keywords

abstract attributes noeq unopteq andbegin by default effect else end ensures exception exists false forall fun function if in include inline inline_for_extraction irreducible logic match module mutable new new_effect noextract of open opaque private range_of reifiable reify reflectable requires set_range_of sub_effect synth then total true try type unfold unfoldable val when with not

Language features

Feature	Supported	Token
Binary Literals	✓
Integers	✓
Floats	✓
Hexadecimals	✓
Octals	✓
Conditionals	✓
Functions	✓
Booleans	✓	true false
Print() Debugging	✓	FStar.IO.print_string