F*: Verification system for effectful programs
F* website
More information on F* can be found at www.fstar-lang.org
Installation
See INSTALL.md
Tutorial
The F* tutorial provides a first taste of verified programming in
F*, explaining things by example.
Wiki
The F* wiki contains additional, usually more in-depth, technical
documentation on F*.
Editing F* code
You can edit F* code using your favourite text editor, but Emacs, Visual Studio
Code, Atom, and Vim have extensions that add special support for F*, including
for instance syntax highlighting, code completion, quick navigation, type hints,
and interactive development. More details on editor support on the F* wiki.
You can also edit simple examples directly in your browser by using
either the online F* editor that's part of the F* tutorial or our
new even cooler online editor (experimental).
Extracting and executing F* code
By default F* only verifies the input code, it does not compile or execute it.
To execute F* code one needs to translate it for instance to OCaml or F#,
using F*'s code extraction facility---this is invoked using the
command line argument --codegen OCaml or --codegen FSharp.
More details on executing F* code via OCaml on the F* wiki.
Also, code written in a C-like shalowly embedded DSL can be extracted to
C
or WASM
by the KreMLin tool,
and code written in an ASM-like deeply embedded DSL can be extracted
to ASM by the Vale tool.
Chatting about F* on Zulip
Users can chat about F* or ask questions at https://fstar.zulipchat.com
(Zulip is a good open source alternative to Slack)
Community mailing list
The fstar-club mailing list is where
various F* announcements are made to the general public (e.g. for
releases, new papers, etc) and where users can ask questions, ask for
help, discuss, provide feedback, announce jobs requiring at least 10
years of F* experience, etc.
List archives are public and searchable, but only members can post.
Join here!
Blog
The F* for the masses blog is also expected to become an important
source of information and news on the F* project.
Reporting issues
Please report issues using the F* issue tracker on GitHub.
Before filing please use search to make sure the issue doesn't already exist.
We don't maintain old releases, so if possible please use the
online F* editor or directly the GitHub sources to check
that your problem still exists on the master branch.
Contributing
See CONTRIBUTING.md
License
F* is released under the Apache 2.0 license; for more details
see LICENSE