Verification system for effectful programs
More information on F* can be found at www.fstar-lang.org
See INSTALL.md
An online book Proof-oriented Programming In F* is in the works and regular updates are
posted online. The book is available as a PDF, or you can read it while trying out
examples and exercises in your browser interface from this tutorial page.
The F* wiki contains additional technical documentation on F*, and is especially useful
for topics that are not yet covered by the book.
You can edit F* code using various text editor. Emacs has the best support currently,
providing syntax highlighting, code completion and navigation, and interactive development,
using fstar-mode.el. However, other editors also have limited support.
More details on editor support are available on the F* wiki.
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 shallowly embedded DSL can be extracted to
C
or WASM
by the KaRaMeL tool,
and code written in an ASM-like deeply embedded DSL can be extracted
to ASM by the Vale tool.
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 contact the mailing list mentioned
below.
Users can also chat about F* or ask questions at this Zulip
forum.
We also have a mailing list which we use mainly for announcements.
Please report issues using the F* issue tracker on GitHub.
Before filing please 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.
See CONTRIBUTING.md
F* is released under the Apache 2.0 license; for more details
see LICENSE