F*: the programming language where proofs are built into the code

Hacker News is discussing F* (pronounced “eff-star”) — a general-purpose, proof-oriented programming language. Its central idea is that a program's correctness is verified not by tests, but by a rigorous mathematical proof built right into the source text.

How it works

F supports both purely functional and “effectful” styles of programming. Its expressiveness comes from dependent types, while proof automation is built on SMT solvers and the tactics of interactive theorem proving. By default, F programs compile to OCaml, but individual fragments can be extracted to F#, C, WebAssembly (with the KaRaMeL tool) or even assembly through the Vale toolset. The compiler itself is written in F* and bootstrapped through OCaml.

The project is distributed under the Apache 2.0 license, is open on GitHub and is actively developed by Microsoft Research, Inria and the community. There are ready-made builds for Windows, Linux and macOS, installation via OPAM, Docker and Nix, as well as an online book in progress, “Proof-oriented Programming In F*,” with examples you can try right in the browser.

Where it's already used

The most interesting part is that formally proven F code is not an academic exercise but components running in production. An umbrella project, Project Everest, has grown up around F, dedicated to secure communication. Out of it came the HACL* library of cryptographic primitives, the proven ValeCrypt assembly implementations and EverCrypt, the provider that unifies them. This code is used in the Mozilla Firefox browser, the Linux kernel, the Python language, the mbedTLS library, the Tezos blockchain, the ElectionGuard e-voting SDK and the WireGuard VPN.

EverParse deserves a separate mention — a generator of binary-format parsers that emits C code proven correct. It is exactly what generated the parsers in Windows Hyper-V: every network packet passing through the Azure cloud is first parsed and checked by code from EverParse.

Research and AI

F remains a live research topic — from the foundations of type and effect theory (Dijkstra monads, the Steel and Pulse concurrent separation logics) to applications in cryptography: verified implementations of TLS 1.3, QUIC, the Signal protocol and MLS. There is work on verifying Rust code by translation into F, a proven garbage collector for OCaml and the verified StarMalloc memory allocator.

In recent years machine learning has been closing in on F* as well: a dataset of 940 thousand lines of code and proofs has been assembled for training models to automatically synthesize proofs, and 3DGen agents are learning to turn text specifications such as RFCs into verifiable format parsers.

Source: Hacker News