$\text{F}^*$ : A Versatile, Proof-Centric Programming Language

$\text{F}^*$ (spoken as "F star") is a general-purpose language designed for proof-oriented programming. It is uniquely capable of supporting both purely functional paradigms and programming with effects.

The language achieves its power by merging dependent types with sophisticated proof automation, leveraging both SMT solving and interactive, tactic-based theorem proving.

🛠️ Compilation and Extraction

$\text{F}^*$ code can be transformed into several other languages depending on the target environment:

Extraction Tool	Target Output
`KaRaMeL`	$\text{F}\#$ , $\text{C}$ , or $\text{Wasm}$
`Vale` toolchain	Assembly

🚀 Getting Started

$\text{F}^*$ is an open-source project hosted on GitHub, maintained through a collaboration between Inria, Microsoft Research, and a global community of contributors.

Installation Options

Depending on your OS (Windows, Linux, or Mac OS X), you can get $\text{F}^*$ via:

Downloading pre-built binaries from the GitHub releases page.
Using the OPAM package manager.
Deploying via Docker.
Installing through Nix.
Compiling from the source code (refer to INSTALL.md).

Educational Resources

If you are looking to master $\text{F}^*$ , the following resources are available:

The Primary Text: An evolving online book titled Proof-oriented Programming In F*. (Clicking the image in the original source allows for in-browser exercises).
Low*: A specialized tutorial for the Low* subset, which is optimized for $\text{C}$ compilation via KaRaMeL.
Academic Courseware: Materials from various seasonal schools, including:
- OPLSS (2021): Embedding Proof-oriented Languages (Notes, slides, and code).
- ECI 2019: Formal Verification using $\text{F}^*$ and $\text{Meta-F}^*$ .
- OPLSS (2019): Security and Correctness in Low-Level Code.
- EUTypes (2018): Program Verification (Ohrid, Macedonia).

👥 Community Engagement

The $\text{F}^*$ community is moving toward centralized, public communication:

Questions & News: Please utilize GitHub Discussions.
Real-time Chat: ~~Slack~~ $\rightarrow$ Zulip (The community is consolidating here).
Events: The F PoP Up Seminar* is a monthly (though occasionally irregular) meeting for developers and users.
Direct Contact: Reach the maintainers at fstar-maintainers@googlegroups.com.

💼 Practical Applications

$\text{F}^*$ is employed extensively in both academic research and industrial production.

Project Everest

Project Everest serves as an umbrella for creating high-assurance, secure communication software. Much of the $\text{F}^*$ language's evolution has been driven by the requirements of this project.

HACL*: A library of cryptographic primitives written in $\text{F}^*$ and extracted to $\text{C}$ .
ValeCrypt: Verified assembly implementations of crypto primitives using the Vale framework embedded in $\text{F}^*$ .
EverCrypt: A unified provider combining the strengths of both HACL* and ValeCrypt.

Production Implementations include:

The Linux kernel & Python
Mozilla Firefox & mbedTLS
The Tezos blockchain
Wireguard VPN & ElectionGuard SDK

EverParse

EverParse is a generator for binary format parsers. It takes formally proven $\text{F}^*$ specifications and extracts them into $\text{C}$ code.

Azure Cloud: Used in Windows Hyper-V to validate every network packet.
Other: Integrated into ebpf-for-windows.

🔬 Research Contributions

$\text{F}^*$ is a focal point for research in formal methods, security, and programming languages. Key papers include:

Language Design & DSLs

The Core: Dependent Types and Multi-monadic Effects in F* (POPL 2016) — The foundational reference for the system.
Low-Level: Verified Low-level Programming Embedded in F* (ICFP 2017) — Detailing the Low* fragment.
Assembly: A Verified, Efficient Embedding of a Verifiable Assembly Language (POPL 2019) — Introducing Vale.
Metaprogramming: Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms (ESOP 2019) — The engine behind typeclasses and tactics.
Effects: Programming and Proving with Indexed Effects (TR 2021) — The logical core and user-defined effects.
Concurrency: Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic (ICFP 2021) — Imperative programs and concurrency via SteelCore.

Semantics & Effect Systems

The research also delves into the mathematical underpinnings of effects:

Dijkstra Monads: Verifying Higher-order Programs with the Dijkstra Monad (PLDI 2013) introduced the core effect system.
Automation: Dijkstra Monads for Free (POPL 2017) demonstrated the automatic derivation of these monads via continuation-passing transformations.

(* Example of a hypothetical F* type signature *)
val verify_packet : p:packet -> Pure (bool)

For a full list of citations, please refer to the official bibliography or contact the maintainers.

F∗\text{F}^*F∗: A Versatile, Proof-Centric Programming Language