Fstar
1 program
Added 2026-03-13T03:15:54Z
Agent: claude-codeModel: claude-sonnet-4-6WebSearch: disabled
Evidence
Report issue
View issues
Aliases: F*, F star, FStar
Provenance: commit 9bae8d3b63 · authored 2026-03-13T04:16:16+01:00 · agent claude-code · model claude-sonnet-4-6
Sources mentioning this language
9 sources · pl_id:
pl/fWikipedia infobox ↗
Pulled from the
wikimedia/structured-wikipedia
snapshot — see data/raw/wikipedia_pl_facts.*.jsonl and
pl_fact.csv for the long-table provenance.
| Paradigms | multi-paradigm: functional · imperative |
|---|---|
| Typing | dependent, inferred, static, strong |
| Designed by | Microsoft Research · Inria · Nikhil Swamy · Juan Chen · Cédric Fournet · Pierre-Yves Strub · Karthikeyan Bhargavan · Jean Yang |
| First appeared | 2011 |
| Influenced by | Dafny · F# · Lean · OCaml · Rocq · Standard ML |
| License | Apache 2.0 |
| Implemented in | F* |
| Homepage | http://fstar-lang.org |
Extensions claimed by this language
5 claims. Each row is one upstream assertion with its strength.
SWH column shows file occurrences with that extension across the entire archive.| Extension | Source | Strength | SWH |
|---|---|---|---|
.fst | linguist | primary | 326.0K files |
.fst | pygments | primary | 326.0K files |
.fsti | linguist | secondary | 17.1K files |
.fsti | pygments | secondary | 17.1K files |
.fst | wikipedia | proposed | 326.0K files |
Related languages
LLM-contributed programs
Factorial
Provenance: commit 9bae8d3b63 · authored 2026-03-13T04:16:16+01:00 · agent claude-code · model claude-sonnet-4-6 · WebSearch disabled
module Factorial
val factorial : n:nat -> Tot nat
let rec factorial n =
if n = 0 then 1
else n * factorial (n - 1)
let main () : FStar.All.ML unit =
let result = factorial 10 in
FStar.IO.print_string ("10! = " ^ string_of_int result ^ "\n")
Real programs from Software Heritage
No SWH evidence indexed yet for this language. (Either the SWH mining hasn't reached this language's extensions, or no matching files exist in the archive.)