Its type system is the proof language/metatheory for making propositions, and its programs are their proofs, and there’s an intermediate form, core F*, that we elaborate to, a partial evaluation phase where we actually use the dependent types to simplify our AST, then codegen/lowering. In your analogy, I would call their core IR the bridge I guess? To clarify, I’m not trying to be a dick, I’m trying to sus out if I’ve understood you correctly