GoKawiilIntroduction F* (pronounced F star ) is a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming. It combines the expressive power of dependent types with proof automation based on SMT solving and tactic-based interactive theorem proving. F* programs compile, by default, to OCaml. Various fragments of F* can also be extracted to F#, to C or Wasm by a tool called KaRaMeL, or to assembly using the Vale toolchain. F* is implemented in F* and bootstrapped using OCaml. F* is open source on GitHub and is under active development by Microsoft Research, Inria, and by the community.
Download F* is distributed under the Apache 2.0 license. Binaries for Windows, Linux, and Mac OS X are posted regularly on the releases page on GitHub. You can also install F* from OPAM, Docker, Nix, or build it from sources, by following the instructions in INSTALL.md.
Community Please use GitHub Discussions to ask questions about F*, learn about announcements, etc. Although we previously used a Slack instance, we aim to consolidate our online community on this public forum on Zulip. We also have a mailing list, which has very low traffic. You can subscribe at fstar-mailing-list. The F* PoP Up Seminar, a users and developers meeting is open to all. We aim to schedule it once a month, though the schedule is irregular---we hope to see you there! You can also contact the maintainers of F* at [email protected].