F* – A Proof-Oriented Programming Language

Original Article ↗ Hacker News Discussion ↗

F\* is presented as a proof-oriented, ML-style language that brings dependent types and formal verification closer to practical software development, with tooling that can extract “human-readable C” used in components of TLS, cryptographic libraries, and major systems like Linux, Firefox, Windows, and Azure. Commenters compare it to F#, Lean, Coq, Idris, and SPARK/Ada, weighing trade-offs in IDE support, compilation targets, verification power, and suitability for general-purpose or safety-critical work. A recurring theme is the tension between the strong guarantees afforded by formal proofs and the complexity, tooling gaps, and scale challenges that currently limit widespread adoption beyond specialized domains such as cryptography and embedded systems.

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.