F* – A Proof-Oriented Programming Language

Original Article ↗ Hacker News Discussion ↗

Scope and goals of F*

  • Positioned as an ML-like, proof-oriented language with dependent types.
  • Emphasizes program verification over pure math formalization.
  • Uses SMT solvers plus tactics and metaprogramming.
  • Type checking is intentionally powerful/undecidable; supports extensional equality.
  • Extracts to “human-readable C” (via the renamed Kremlin → Karamel tool) and also to OCaml and other mainstream targets.

Relationship to F#, OCaml, and other languages

  • Syntax and “feel” are OCaml/F#-like; name is historically tied to the “F” lineage (System F, F#, etc.).
  • Not a CLR/.NET language by default, though some are interested in .NET integration.
  • Compared with SPARK/Ada: F* uses dependent types; SPARK’s contracts can be statically checked too.
  • Compared with Coq/NuPRL: stronger focus on compilation and programming, plus SMT integration.
  • Compared with Lean: Lean is praised as a language but is currently math-centric; lacks libraries and tactics for large-scale code verification.

Tooling and IDE experience

  • Earlier lack of mainstream IDE support was a real adoption barrier.
  • Now has VS Code and Emacs modes; some say Copilot works well with it.
  • Parallel discussion on F# tooling: modern Ionide/Rider/VS are seen as good, but earlier experiences (especially cross‑platform) were rough.

Real-world use and Project Everest

  • F* predates but was heavily advanced by Project Everest.
  • Verified components include TLS/QUIC pieces, parsers, and cryptographic primitives.
  • These are reported as deployed in Windows kernel, Linux, Firefox, Python, Azure, and embedded crypto.

Practicality of formal verification

  • Some doubt feasibility for very large (10M+ LOC) systems; others argue automation and good tactics make large proofs possible in principle.
  • Suggested strategy: prove small components, rely on strong encapsulation, and combine proofs with property-based and ordinary tests.
  • Lean 4 is seen as usable as a general-purpose language, but currently poor for verifying real-world code due to missing tactic libraries.

Culture, naming, and adoption

  • Discussion around renaming “Kremlin” to “Karamel” touches on Soviet/Russian imagery, changing political context, and project branding risk.
  • Many commenters are drawn to dependent types “like moths to a flame,” but note that jobs and organizational approval for such languages remain rare.