F*: A general-purpose proof-oriented programming language
Points and comments are a snapshot, not live.
F* is a general-purpose proof-oriented language combining dependent types with SMT automation.
F* (F star) compiles by default to OCaml, with fragments extractable to F#, C, Wasm, or assembly via KaRaMeL and Vale. It is developed by Microsoft Research, Inria, and the community under Apache 2.0. Key projects include HACL* (verified cryptographic primitives used in Firefox, Linux kernel, Python, mbedTLS, Tezos, ElectionGuard, Wireguard), EverParse (binary format parsers hardened in Windows Hyper-V and Azure), and EverCrypt. Research spans dependent types, multi-monadic effects, Low* (low-level subset), Steel (concurrent separation logic), and Meta-F* (tactics and metaprograms).
What commenters are saying
Several commenters praised F* for its ability to express calls to external libraries during incremental migration of C codebases. The top-voted complaint was that the website buries code examples; users wanted syntax visible on the homepage. Others countered that the interactive tutorial is one click away and that syntax is the least interesting part of F*. A subthread debated indentation-based languages. One commenter asked whether F* is suitable for verifying compilers; two replies affirmed it is. Another questioned F*'s handling of basic arithmetic, comparing it unfavorably to Lean.