Repository files navigation

More information on F* can be found atwww.fstar-lang.org

SeeINSTALL.md

An online bookProof-oriented Programming In F* is in the works and regular updates areposted online. The book is available as aPDF, or you can read it while trying outexamples and exercises in your browser interface from thistutorial page.

TheF* wiki contains additional technical documentation on F*, and is especially usefulfor 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,usingfstar-mode.el. However, other editors also have limited support.More details oneditor support are available on theF* 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 thecommand line argument--codegen OCaml or--codegen FSharp.More details onexecuting F* code via OCaml on theF* wiki.

Also, code written in a C-like shallowly embedded DSL can be extracted toCorWASMby theKaRaMeL tool,and code written in an ASM-like deeply embedded DSL can be extractedto ASM by theVale tool.

The F* developers and many users interact on thisSlackforum---you should be able tojoin automatically byclickinghere,but if that doesn't work, please contact the mailing list mentionedbelow.

Users can also chat about F* or ask questions at thisZulipforum.

We also have amailing list which we use mainly for announcements.

Please report issues using theF* 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 theonline F* editor or directly the GitHub sources to checkthat your problem still exists on themaster branch.

SeeCONTRIBUTING.md

F* is released under theApache 2.0 license; for more detailsseeLICENSE