F*: A general-purpose proof-oriented programming language

F*编程语言正式发布，微软研究院联合法国国家信息与自动化研究所，给大家带来了一款能“自我证明”的编程工具。它的最大亮点在于：程序员写完代码后，F*能像数学证明一样自动检查逻辑漏洞，让程序在运行前就被验证是正确的，从根源上杜绝bug。听起来很玄乎？其实可以这样理解：传统编程像是“写完再测试”，而F*变成了“边写边推理”。它能借助强大的自动证明技术，把代码的安全性质变成可验证的数学公式。就像盖房子时，设计师用结构力学计算每根梁的承重，而不是等房子塌了再修。F*甚至能编译成C语言或WebAssembly，适合开发底层系统。这项技术对普通人的影响，藏在那些“不能出错”的软件里——比如银行转账系统、医疗设备控制、自动驾驶程序。有了F*，开发者可以证明这些代码不会越界、不会泄露数据，我们使用的数字服务将更安全可靠。虽然对普通用户来说感知不强，但软件质量提升，意味着更少的崩溃、更少的信息泄露，也意味着未来的智能设备能更放心地交给我们使用。

Introduction Download Learn Community Uses Research People Introduction 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. Download 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. Learn F* 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. Low* We also have a tutorial that covers Low*, a low-level subset of F*, which can be compiled to C by KaRaMeL. Course Material F* courses are often taught at various seasonal schools. Lectures and course materials for some of them are also a useful resource. Embedding Proof-oriented Programming Languages in F* Online lectures at the Oregon Programming Language Summer School (2021): Lecture notes, slides, code Formal Verification with F* and Meta-F* Lectures and tutorial at ECI 2019: Lecture notes, slides, code Verifying Low-Level Code for Correctness and Security Lectures at the Oregon Programming Language Summer School (2019): Lecture notes, slides, code Program Verification with F* Course at 2018 EUTypes Summer School, 8-12 August, 2018, Ohrid, Macedonia Course material Community Please use GitHub Discussions to ask questions about F*, learn about announcements, etc. Although we previously used a Slack instance, we aim to consolidate our online community on this public forum on Zulip. We also have a mailing list, which has very low traffic. You can subscribe at fstar-mailing-list. The F* PoP Up Seminar, a users and developers meeting is open to all. We aim to schedule it once a month, though the schedule is irregular---we hope to see you there! You can also contact the maintainers of F* at fstar-maintainers@googlegroups.com. Uses F* is used in several projects in both industrial and academic settings. We list a few of them here. If you are using F* in your project, please let us know by writing to the fstar-mailing-list. Project Everest Project Everest is an umbrella project that develops high-assurance secure communication software in F*. A big part of the development of F* has been motivated by the scenarios that Project Everest targets. Several offshoots from Project Everest continue as their own projects, including some of those listed below. HACL*, ValeCrypt, and EverCrypt HACL* is a library of high-assurance cryptographic primitives, written in F* and extracted to C. ValeCrypt provides formally proven implementations of cryptographic primitives in Vale, a framework for verified assembly language programming embedded in F*. EverCrypt combines them into a single cryptographic provider. Code from these projects is now used in production in several projects, includ