Giter Club home page Giter Club logo

fstar's Introduction

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

fstar's People

Contributors

a-manning avatar aa755msr avatar ad-l avatar artagnon avatar aseemr avatar catalin-hritcu avatar cpitclaudel avatar darrenge avatar dzomo avatar fournet avatar gugavaro avatar jaybosamiya avatar jkzinzindohoue avatar jroesch avatar kyodralliam avatar mlr-msft avatar monal avatar msprotz avatar mtzguido avatar mwhicks1 avatar nikswamy avatar protz avatar qunyanm avatar s-zanella avatar strub avatar tahina-pro avatar tchajed avatar victor-dumitrescu avatar wintersteiger avatar zoep avatar

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.