F*: A general-purpose proof-oriented programming language for verified software

Introduction to F*

F* is a general-purpose, proof-oriented programming language that combines dependent types with proof automation through SMT solving and interactive theorem proving. It supports both purely functional and effectful programming paradigms.

Compilation and Development

F* programs compile to OCaml by default, with fragments extractable to F#, C, or WebAssembly via KaRaMeL, and to assembly using the Vale toolchain. The language itself is implemented in F* and bootstrapped with OCaml. It is an open-source project actively developed by Microsoft Research, Inria, and a community of contributors.

Availability and Learning Resources

F* is distributed under the Apache 2.0 license, with binaries available for Windows, Linux, and macOS on GitHub. Installation is also possible via OPAM, Docker, Nix, or by building from source. Learning resources include an online book, 'Proof-oriented Programming In F*', and tutorials for Low*, a subset of F* that compiles to C.

Real-world Applications

F* is applied in various industrial and academic projects. Notably, it is central to Project Everest, an initiative focused on developing high-assurance secure communication software. This includes projects like HACL*, a library of cryptographic primitives extracted to C, and ValeCrypt, which provides formally proven cryptographic implementations in assembly language.