F*'s type system includes dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact specifications for programs. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and interactive proofs.
F* is written entirely in F*, and bootstraps via OCaml. It is open source and under active development on GitHub. A detailed description of the current F* variant is available in a series of POPL and ICFP papers (2016, 2017, 2018, 2019, and 2020). You can learn more about F* by following the online tutorial and reading our papers. Materials from recent talks are also available below.
Community: Please use the GitHub Discussions list to ask questions about F*, learn about announcements, etc. Although we have only recently started using GitHub Discussions, we hope it will become the primary way to engage with the F* community and also an archive of questions & answers that are of general interest.
The F* developers and many users interact on this Slack forum---you should be able to join automatically by clicking here, but if that doesn't work, please ask for access on this thread.
There is also a public forum on Zulip.
The F* PoP Up Seminar, a monthly F* users and developers meeting is open to all---we hope to see you there!