Skip to content

qunyanm/FStar

This branch is 16275 commits behind FStarLang/FStar:master.

Folders and files

NameName
Last commit message
Last commit date

Latest commit

author
Dzomo the everest Yak
Jun 17, 2019
4e24164 · Jun 17, 2019
Dec 11, 2017
May 6, 2019
Jun 5, 2019
Jan 27, 2017
Jun 4, 2019
May 9, 2019
Nov 12, 2018
Jun 13, 2019
Jun 14, 2019
Jun 14, 2019
Mar 29, 2019
Jun 15, 2019
Nov 12, 2018
Feb 17, 2019
Feb 15, 2018
Aug 17, 2017
May 15, 2018
Jan 27, 2017
Apr 9, 2019
May 19, 2019
Jun 4, 2019
Jan 27, 2017
Jan 27, 2017
Jan 28, 2019
May 19, 2019
May 15, 2018
Mar 5, 2019
May 6, 2019
May 18, 2018

Repository files navigation

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, Atom, and Vim have extensions that add special support for F*, including syntax highlighting 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

About

Verification system for effectful programs

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • F* 66.5%
  • F# 27.7%
  • OCaml 3.9%
  • C 0.6%
  • Shell 0.4%
  • Python 0.4%
  • Other 0.5%