Thomas Gazagnaire

Last week I attended the F Prime workshop at JPL, over 100 people, from CubeSat student teams to flagship mission engineers. I learned a lot about F Prime, and I kept noticing how familiar the concepts felt. This post is some of my thoughts on why.

F Prime (GitHub) is NASA's open-source framework for building reusable flight software. Before it, most missions started from scratch or copy-pasted code from previous ones. It already flies on Ingenuity (Mars Helicopter), CADRE (autonomous lunar rovers), and Europa Clipper. It is trying to bring standard software engineering practices (modularity, unit testing, reusability, continuous integration) to a domain that has historically resisted them.

The framework has its own modelling language called FPP (F Prime Prime). You describe your system in FPP (components, ports, state machines, topologies) and the toolchain generates thousands of lines of C++ for you (plus a fair amount of CMake glue to wire the build together). That is the point: you write the architecture, not the boilerplate. If you have ever worked with MirageOS, all of this should sound oddly familiar.

For those who do not know, MirageOS (GitHub) is a library operating system where the entire application, from the network stack to the storage layer, is built from OCaml modules wired together by functors. The runtime is minimal (Solo5 provides about ten hypercalls), no general-purpose OS, no libc, just typed interfaces all the way down. Our ASPLOS 2013 paper received the Influential Paper Award in 2025. I think F Prime and MirageOS share a surprising number of ideas. Here is how I see the two relate.

Components are module types. In F Prime, you define a component by declaring its ports, typed interfaces that connect it to the rest of the system. The FPP paper puts it nicely: a port "has a type and a kind; the type is like a function signature." Components have no compile- or link-time dependencies on each other: each component depends only on the types of the ports that it uses.

FPP distinguishes three kinds of components: passive (called synchronously by the caller), queued (has an internal message queue but no thread of its own), and active (has its own thread that drains its queue). This is a concurrency model baked into the component types:

passive component Thermometer {
  sync input port cmdIn: Fw.Cmd
  output port tlmOut: Fw.Tlm
  telemetry Temperature: F32
}

module type THERMOMETER = sig
  type t
  val cmd_in : t -> Cmd.t -> unit
  val tlm_out : t -> Tlm.t
  val temperature : t -> float
end

Both say the same thing: anything that calls itself a thermometer must accept commands, emit telemetry, and report a temperature. The ports are the function signatures. The component type is the module type.

The mapping is suggestive, not exact. FPP ports have directionality (input vs output) and invocation kinds (sync, async, guarded) that a flat OCaml signature does not enforce. In MirageOS we used phantom types on device connectors to recover some of this structure (see Radanne, Gazagnaire et al., 2019) but the parallel is clear enough to be useful.

The concurrency story is interesting too. F Prime's active/passive/queued distinction maps loosely to what OCaml has been working through for years. A passive component is a plain function call. An active component has its own thread that drains a message queue. Compare:

active component Logger {
  async input port logIn: Fw.Log
}

module type LOGGER = sig
  type t
  val log_in : t -> Log.t -> unit Lwt.t
end

In FPP, a component is either passive, queued, or active. In OCaml, you can mix synchronous and asynchronous functions in the same module signature: some values return unit, others return unit Lwt.t. The concurrency model is per-function, not per-component. Queued components sit in between, an event loop without a dedicated thread. OCaml has been moving from monadic concurrency (Lwt.t) to effect handlers in OCaml 5, which delegate scheduling to a library like Eio without colouring every type signature. F Prime bakes the concurrency model into the component kind; OCaml delegates it to the application scheduler.

State machines are GADTs. This one is not specific to MirageOS, it is about OCaml's type system more broadly. FPP has built-in state machine support (states, signals, guards, and transitions). Here is a door controller (from the FPP User's Guide):

state machine Door {
  signal open
  signal close
  guard isLocked

  initial enter Closed

  state Closed {
    on open if isLocked enter Closed
    on open enter Open
  }

  state Open {
    on close enter Closed
  }
}

FPP: a door with two states and a guard.

The generated state machine diagram.

In OCaml, you can encode the same transitions as a GADT. The type parameters track which state you are in and which state a signal takes you to:

type closed
type opened

type _ state =
  | Closed : closed state
  | Open : opened state

type (_, _) signal =
  | Open  : (closed, opened) signal
  | Close : (opened, closed) signal

type guard = Locked | Unlocked

let step : type a b. a state -> (a, b) signal -> guard
    -> (b state, a state) result =
  fun state signal guard ->
    match state, signal, guard with
    | Closed, Open, Locked   -> Error state
    | Closed, Open, Unlocked -> Ok Open
    | Open, Close, _         -> Ok Closed

The type (closed, opened) signal means: this signal is only valid from the closed state, and it produces the opened state. Try to close an already-closed door and the compiler rejects it. The guard is a runtime check (just like in FPP), but the result type makes the self-loop explicit: Error state means the guard blocked and you stayed where you were. FPP's state machine compiler does the same checks at the FPP level; the GADT pushes them into OCaml's own type system.

The wiring is where they diverge. How you describe the way all these components connect into a running system is where the two frameworks take different paths.

In F Prime, you define a topology: a wiring diagram that connects component instances through their ports, the way an engineer connects chips on a board. Sub-topologies let you group and reuse partial wirings (think of them as sub-circuits). The FPP compiler checks that port types match, then the autocoder generates C++ and a fair amount of CMake glue. For the final assembly, users customise init sequences, thread priorities, and buffer sizes through C++ templates and build rules. There are many knobs to turn.

topology Mission {
  instance sensor: Sensors.Thermometer
  instance dispatcher: Svc.CmdDispatcher

  connections command {
    dispatcher.compCmdSend -> sensor.cmdIn
  }
}

module Mission
    (Sensor : THERMOMETER)
    (Dispatcher : CMD_DISPATCHER) = struct
  let dispatch sensor cmd =
    Sensor.cmd_in sensor cmd
  let init sensor =
    Dispatcher.register (dispatch sensor)
end

In MirageOS, a functor is a function from modules to modules: you pass a module satisfying some signature, and you get a new module back. The functor is the sub-topology. People write functor applications by hand all the time in OCaml, and it works fine. But in MirageOS we wanted to automate redeployment across different hypervisors and driver sets (Xen, KVM, Solo5, each with their own network and storage stacks), so we built Functoria, an eDSL that describes the assemblage and generates the build rules and functor applications for each target. That is structurally closer to what F Prime's autocoder does: both take a high-level wiring description and produce glue code for a specific target.

Both check that the wiring is type-correct, but in different places: FPP in its own compiler, OCaml in the host language's type system. FPP gives you a graph-oriented model that maps naturally to how electronic engineers think. Functoria gives you composability (functors are first-class language constructs), but the resulting code can get... involved. (Who said Irmin in the back? :p)

The unit of compute seems settled: small typed components, explicit async I/O, function types as interfaces. The global wiring is not. I have seen it spawn build system rules (Makefile spaghetti), domain-specific languages (FPP, Functoria), and language-specific support (functors). Parnas (1972) told us to hide information behind interfaces. Nobody told us how to wire a thousand of them together ;-)