Comment by rng_civ

Have you taken a look at the paper "Foreign Function Typing: Semantic Type Soundness for FFIs" [0]?

> We wish to establish type soundness in such a setting, where there are two languages making foreign calls to one another. In particular, we want a notion of convertibility, that a type τA from language A is convertible to a type τB from language B, which we will write τA ∼ τB , such that conversions between these types maintain type soundness (dynamically or statically) of the overall system

> ...the languages will be translated to a common target. We do this using a realizability model, that is, by up a logical relation indexed by source types but inhabited by target terms that behave as dictated by source types. The conversions τA ∼ τB that should be allowed, are the ones implemented by target-level translations that convert terms that semantically behave like τA to terms that semantically behave like τB (and vice versa)

I've toyed with this approach to formalize the FFI for TypeScript and Pyret and it seemed to work pretty well. It might get messier with Rust because you would probably need to integrate the Stacked/Tree Borrows model into the common target.

But if you can restrict the exposed FFI as a Rust-sublanguage without borrows, maybe you wouldn't need to.

[0] (PDF Warning): https://wgt20.irif.fr/wgt20-final23-acmpaginated.pdf