Top 1,000 Features Creators Events Podcasts Extensions Blog Explorer CSV Download


< >

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

#118on PLDB 10Years Old 250Repos
Download source code:
git clone

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...

Example from hello-world:
module Hello let main = FStar.IO.print_string "Hello World\n"
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 Example
Binary Literals โœ“
Integers โœ“
Floats โœ“
Hexadecimals โœ“
Octals โœ“
Conditionals โœ“
Functions โœ“
Booleans โœ“ true false
Print() Debugging โœ“ FStar.IO.print_string

View source

- Build the next great programming language ยท About ยท Resources ยท Acknowledgements ยท Part of the World Wide Scroll