Article URL: https://fstar-lang.org/ Comments URL: https://news.ycombinator.com/item?id=49143925 Points: 40 # Comments: 12

F* (pronounced F star) is a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming. It combines the expressive power of dependent types with proof automation based on SMT solving and tactic-based interactive theorem proving. F* programs compile, by default, to OCaml. Various fragments of F* can also be extracted to F#, to C or Wasm by a tool called KaRaMeL, or to assembly using the Vale toolchain. F* is implemented in F* and bootstrapped using OCaml. F* is open source on GitHub and is under active development by Microsoft Research, Inria, and by the community. F* is distributed under the Apache 2.0 license. Binaries for Windows, Linux, and Mac OS X are posted regularly on the releases page on GitHub. You can also install F* from OPAM, Docker, Nix, or build it from sources, by following the instructions in INSTALL.md. An online book Proof-oriented Programming In F* is being written and regular updates are posted online. You probably want to read it while trying out examples and exercises in your browser by clicking the image below. We also have a tutorial that covers Low*, a low-level subset of F*, which can be compiled to C by KaRaMeL. F* courses are often taught at various seasonal schools. Lectures and course materials for some of them are also a useful resource. Please use GitHub Discussions to ask questions about F*, learn about announcements, etc.