F*: A general-purpose proof-oriented programming language
Summary
F* is a general-purpose proof-oriented programming language that blends dependent types with SMT-based proof automation and interactive tactics. It targets OCaml by default and can extract to F#, C, or Wasm via KaRaMeL; the project is open-source with contributions from Microsoft Research and Inria, and is tied to cryptographic libraries and verified code such as HACL*, EverCrypt, and EverParse.