F*: A Proof-Oriented Programming Language That Compiles to C, Wasm, and Assembly
F*: A general-purpose proof-oriented programming language
F* is a general-purpose proof-oriented programming language that combines dependent types with SMT-based proof automation and tactic-based interactive theorem proving. It compiles to OCaml by default, and fragments can be extracted to C, Wasm, or assembly via tools like KaRaMeL and Vale. Developed by Microsoft Research, Inria, and the community, F* is used in high-assurance projects like Project Everest, HACL*, and EverParse, with production deployments in Firefox, the Linux kernel, and Azure.
F* is a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming.
- cyanregiment
Clicked like 5 pages and never found 1 code example.
Idk why languages don't have their syntax in a sandbox front-and-center on the home page.
It's like a video game site with zero screenshots or videos (also rampant).
New programming languages I want 2 things:
1. What does the syntax look like
2. Why would I use this language
Talk about the proof logic, show the syntax, thank you
- LelouBil
- LelouBil
I like Haskell, and to me this seems really useful as a kind of "noob" to functional languages.
Is this used in the industry ? And for what kind of software ?
- pvsnp
I liked being able to express calling external libraries while incrementally migrating existing C codebases to F*. Very solid language.
- boutell
I guess responsive stylesheets can't be implemented without side effects...