How integration with FStar might actually be easier with fsnative

[houstonhaynes]

As the Fidelity Framework matures, we're looking toward integration with F* (F-star), the proof-oriented programming language from Microsoft Research and INRIA. This raises interesting questions about type system alignment that we'd like to explore with the community.

A Tough Nut Becomes Manageable

F* extracts verified code to several targets, with OCaml as the primary, well-maintained path. When we examine what F* expects from its extraction targets, we find that fsnative's type representations align more naturally with F*/OCaml semantics than with .NET's Base Class Library.

This isn't coincidental. F# began as "OCaml for .NET" before developing its own identity. F* draws heavily from OCaml in implementation and semantics. And fsnative, despite its F# syntax, makes semantic choices that echo OCaml's approach to memory and types.

Concrete Type Differences

Consider how fundamental types differ across these systems:

Concept	F*/OCaml	.NET BCL	fsnative
Strings	UTF-8, explicit encoding (BatUTF8)	UTF-16, System.String	UTF-8, NativeStr with deterministic lifetime
Options	Value ADT, stack-allocated	Reference type, heap-allocated FSharpOption<T>	voption, value type, stack-allocated
Tuples	Value, immediate	System.Tuple<> (heap) or ValueTuple<>	struct tuple, stack-allocated
Integers	Explicit width or arbitrary precision (Zarith)	Boxed in generic contexts	Explicit width, never boxed
Arrays	Contiguous, explicit bounds	System.Array with runtime type info	NativeArray<'a>, minimal metadata

The BCL's design reflects the CLR's heritage: everything is an object, reference semantics are the default, and the garbage collector manages lifetimes. These are reasonable choices for a managed runtime, but they create impedance mismatches when F* tries to extract code that assumes value semantics and explicit memory management.

Why This Matters for Verification

F* tracks effects and proves properties about programs. When it extracts to OCaml, those proofs align with how the code actually executes. The extracted code uses value types where F* expects values. Memory behavior is predictable. The proofs remain valid.

Extraction to .NET F# is more fraught. The F* repository documentation is direct: "F# extraction is plagued by some bugs and lags quite a bit behind OCaml extraction." Part of this lag stems from the semantic gap. Every primitive type requires adaptation to BCL semantics that differ from what F* expects.

Consider a simple example: F* proves that a function returns Some x where x satisfies certain properties. In OCaml extraction, Some is a lightweight tag on a value. In .NET extraction, Some becomes a heap allocation, introducing GC behavior that the proof didn't account for. The logical property still holds, but the operational semantics have shifted.

fsnative closes this gap. When F* extracts to fsnative-compatible F#, Some x becomes a ValueSome x, a stack-allocated discriminated union, semantically equivalent to OCaml's representation. The proof about the value's properties maps directly to the runtime behavior.

The F* Integration Path

We're considering a fork of FStarLang/FStar that adds a new extraction target alongside OCaml and .NET F#. The structure would look like:

FStar repository
├── ulib/ml/ # OCaml runtime support (upstream, well-maintained)
├── fsharp/ # .NET F# runtime support (upstream, lags behind)
└── fsnative/ # Native F# runtime support (new, peer to fsharp/)

The fsnative/ directory would contain runtime support modules implementing F* primitives using native types:

• FStar_String.fs , String operations via NativeStr
• FStar_Option.fs , voption operations
• FStar_Bytes.fs , Byte handling with explicit lifetimes
• FStar_Heap.fs , Memory model mapping to regions (Stack, Heap, Arena)
• Prims.fs , Primitive types and operations

Each module implements the same interface as its OCaml counterpart. The translation from F* to fsnative becomes more direct than to .NET F# because fsnative's semantics are closer to what F* already produces for OCaml.

Effect System Alignment

F* tracks effects: Tot (total, pure), ML (may diverge, may have effects), ST (stateful), IO (input/output). These effects carry verification information about what a function may do. fsnative's coeffect system provides a natural mapping:

F* Effect	Meaning	fsnative Mapping
Tot	Total, pure, terminating	Pure function, no coeffects
ML	May diverge, may have effects	General function
ST	Stateful, heap manipulation	Memory region access coeffect
IO	I/O effects	Platform binding coeffect

The mapping preserves information needed for verification while fitting fsnative's native compilation model. When F* proves a function is Tot, that purity proof can guide Firefly's optimization passes, the compiler knows this code has no side effects and can be freely reordered, memoized, or eliminated if unused.

Memory Model Considerations

F* has sophisticated memory models including HyperStack for reasoning about stack and heap allocation. fsnative has memory regions: Stack, Heap, Arena, Peripheral, Flash.

A complete integration would map F* memory reasoning to fsnative regions:

F* Concept	fsnative Equivalent
Stack frames	Stack region
Heap references	Heap region
Eternal references	Arena region
Memory-mapped I/O	Peripheral region

This mapping enables F* proofs about memory safety to carry through to native code. When F* proves that a reference doesn't escape its stack frame, Firefly can allocate it on the stack with confidence. When F* proves array bounds, Firefly can eliminate redundant checks.

Open Questions

We're early in thinking through this integration and would value perspectives from those with experience in:

OCaml and F* extraction: What are the pain points in the current F# extraction path? Where does the semantic mismatch cause the most friction?
Dependent types and verification: How do refinement types and dependent pairs map to representations without runtime type information? F* erases proof-only code, but computational code still needs representation.
Integer semantics: F* uses arbitrary-precision integers (Z.t via Zarith) by default. Should fsnative provide arbitrary precision as the default int type, or require explicit width annotations? This affects verification, unbounded integers simplify proofs but complicate native code generation.
Effect erasure: F* effects guide verification but often erase at extraction. How should the fsnative extraction preserve effect information for Firefly's optimization passes without runtime overhead?

Timeline

This is forward-looking architectural discussion. The F* integration is not yet implemented. Current priorities are solidifying the core Firefly pipeline, FNCS type resolution, and the Alloy standard library. But the type system decisions we make now have downstream consequences. Understanding the OCaml alignment helps us make choices in fsnative that will ease F* integration when the time comes.

If you have experience with F*, OCaml, or proof-carrying code and want to help shape this direction, we'd welcome your input.