Rust's Retrofits

Tyler Mandry opens his RustConf 2026 talk in Montreal, “Beyond the &: A Future for Native Smart Pointers in Rust,” with a dozen lines of Rust that cache rendered pages, and he spends the better part of six minutes on them. The function compiles. When Mandry puts the cache and its template behind a Mutex, rustc rejects the identical body, and a programmer who applies the compiler’s suggested fix still gets the borrow error. Mandry co-leads the Rust language design team, and he uses that small snag to motivate the most ambitious idea in his talk: extending to library-defined pointer types the reasoning that Rust’s compiler applies only to its built-in references and Box.

The Rust Foundation published the talk on October 1, alongside Robert Seacord’s “Unsafe Rust.” Seacord convenes the C standards committee, and he examines unsafe Rust from the standpoint of the automotive safety-related systems built at Woven by Toyota, where he works. A year earlier, at RustConf 2025, Rain of Oxide Computer Company gave “Cancelling Async Rust,” a close study of cancellation in async Rust drawn from production bugs. Read together, the three talks are an account of guarantees being retrofitted onto a language already in wide production, at the edges of its original design.

The timing is hard for us to ignore. Our Clef language has no unsafe keyword. As we departed from F# norms to create our own language, we removed inherited raw pointer types, and our compiler (Composer) receives facts about foreign code as declarations and checks programs against them. We see the boundaries these talks examine can be stated in our specification as compiler obligations. Mandry, Seacord and Rain have each mapped one of those boundaries with real care, and in their maps we found a precise account of the baseline integrity we have planned for the Clef language.

The Guard in the Middle

Mandry’s first version, from his opening slide, receives its state as a plain mutable reference. The borrow checker tracks state.cache and state.template as separate places, so the closure can read the template while the cache entry holds a mutable borrow. Mandry finds it “extremely cool that this function works in a language that’s both 100% safe and as fast as Rust.”

struct RenderState {
    cache: HashMap<String, Arc<String>>,
    template: String,
}

fn render_page(state: &mut RenderState, name: &str) -> Arc<String> {
    // Mutably borrow `state.cache` using the Entry API.
    let entry = state.cache.entry(name.to_string());
    entry.or_insert_with(|| {
        // Create the entry if it doesn't exist.
        Arc::new(state.template.replace("$name", name))
    }).clone()
}

The function compiles under a second rule as well: since the 2021 edition a closure captures only the fields it uses, so from state this one borrows only state.template. We compiled the slide with rustc 1.98, and under the 2018 edition the same function is rejected with error E0502.

In the second version, titled “Shared access with MutexGuard,” the state sits behind a Mutex so that threads can share it. Locking the mutex returns a MutexGuard, an RAII value that holds the lock until it is dropped and exposes the data through its Deref and DerefMut implementations. The body below the lock is unchanged:

fn render_page(state: &Mutex<RenderState>, name: &str) -> Arc<String> {
    let state: MutexGuard<'_, RenderState> = state.lock().unwrap();

    // Mutably borrow `state.cache` using the Entry API.
    let entry = state.cache.entry(name.to_string());
    entry.or_insert_with(|| {
        // Create the entry if it doesn't exist.
        Arc::new(state.template.replace("$name", name))
    }).clone()
}

In our runs under the 2018, 2021 and 2024 editions, rustc rejects it with two errors. The second, E0502, reports that the guard itself is borrowed mutably and immutably at once:

error[E0502]: cannot borrow `state` as immutable because it is also borrowed as mutable
  --> slide2.rs:16:26
   |
15 |     let entry = state.cache.entry(name.to_string());
   |                 ----- mutable borrow occurs here
16 |     entry.or_insert_with(|| {
   |           -------------- ^^ immutable borrow occurs here
   |           |
   |           mutable borrow later used by call
17 |         // Create the entry if it doesn't exist.
18 |         Arc::new(state.template.replace("$name", name))
   |                  ----- second borrow occurs due to use of `state` in closure

In the first version the mutable borrow covered only the field state.cache. Here it covers state, the guard itself. Each access through the guard desugars to a method call: deref_mut for state.cache, which takes the guard by mutable reference, and deref for the closure’s state.template, which takes it by shared reference. The reference that deref_mut returns keeps the guard mutably borrowed for as long as entry lives, and the closure’s shared borrow conflicts with it. Mandry is generous to the compiler here: “Given what the borrow checker can see it is right to complain.”

For the first error, E0596, rustc suggests declaring the binding as let mut state. We applied the suggestion, and rustc then reports only the E0502, on the same lines. Mandry warns against it: the suggestion “leads you down the wrong path and actually does nothing to fix the [borrow] checker error. You don’t need a mutable state binding. What you need is for state to be a mutable reference again.”

His fix replaces the let state line with a plain mutable reference taken through the guard:

let state: &mut RenderState = &mut *state.lock().unwrap();

Two rules of the language govern that line, and we confirmed both by compiling an example for ourselves. Temporary lifetime extension means that the guard, and with it the lock, lives until the end of the enclosing block. Through the plain &mut RenderState, the borrow checker tracks cache and template as disjoint fields again, and under the 2021 capture rule the closure borrows only the template. Compiled as 2018-edition code, the fixed version is rejected as well.

We then tested field-by-field borrowing through two other pointer types. Written against &mut Box<RenderState>, the body compiles. Written against a minimal wrapper whose deref_mut returns its only field, it is rejected with E0502 again. The Rust Reference documents the limit: field-by-field borrowing “does not apply if automatic dereferencing is done through user-defined types other than Box.”

The Cost of Distance

Right after the fix, Mandry sums up the cost of leaving the built-in types, for newcomers and veterans alike:

But moving away from Rust’s built-in types quickly puts you in the realm of having to write your code differently for reasons that are hard to explain, especially to a new Rust programmer. And worse, the farther you get from Rust’s built-in aliasing model, the more dramatically it breaks down. So seasoned Rust developers are used to working around these kinds of snags.

His point concerns ergonomics and the reach of the aliasing model, and he offers it as the case for his proposal. Interop is the far end of that distance. Pointer types that represent C++ references “can’t be Rust references because they have fewer aliasing guarantees,” and his slide shows the raw-pointer round trip that projects a CRef of a struct to a CRef of one of its fields in current Rust:

fn project(cref: CRef<'_, MyStruct>) -> CRef<'_, Field> {
    unsafe {
        CRef::from_ptr(
            &raw const (*cref.as_ptr()).field
        )
    }
}

Mandry spells out the cost, which is paid per field and per pointer variant:

And then we wrap the whole result back up into a CRef. And every single step of this operation is unsafe even though the operation itself is safe, because of the invariants on CRef. But that’s not the worst part. The worst part is we have to implement a function like this for every single field that we want to do this for. And it needs to support not just CRef but CRef’s mutable sibling CMut. And not just CRef and CMut, but pinned versions of each of those. Pinning is very common for C++, and I can go on, but you get the idea. Even with a macro to write this code for you, this kind of API can be incredibly painful to deal with. If you’ve ever used pin-project, it’s like that but on steroids.

CRef is one pointer type among many. Mandry’s slide titled “Pointer types are everywhere” shows ten from the standard library alone, from &T and Box<T> to MutexGuard<T> and NonNull<T>. A later version of the slide adds ecosystem types such as ArcSwap and CRef. He gives the variety its due: “every single one of these types has slightly different semantics. If it didn’t, there would be no reason for it to exist. And I think this really demonstrates the versatility of Rust as a language. But also, there’s a lot going on.” We agree on both counts, and we note that each library type’s contract resides in its implementation, reviewable one type at a time.

A Language of Places

Mandry builds his proposal on a line he delivers in Montreal: “Rust is a language of places.” A place is “somewhere a value lives that you can name,” such as a local variable or one of its fields, and the borrow checker operates on places directly. Built-in references and Box are part of that language. A Deref implementation is a function that returns a reference, with no stated relationship between one call’s result and the next, so in Mandry’s words the borrow checker gets back “a fresh &mut with no well-defined relationship to the guard or to any future call to deref_mut.”

He proposes a handle, a value the compiler constructs for a place expression to describe where the place is. “Many handles are just internally a raw pointer,” and they never appear in ordinary code. Every pointer type has a corresponding handle type, and trait implementations on that handle declare the operations its places support. In the deck’s schematic signatures, the operation traits are all declared unsafe trait:

The access kind is shared, exclusive or untracked, and the timing is a lifetime for reference outputs and an instant for raw ones. Mandry raised one more operation in the Q&A: the discriminant read that a match on an enum through a handle performs. A borrow! macro, perhaps an @ operator later, borrows a place as whatever pointer type inference requires. After borrow checking, the compiler lowers the expression to a call of the handle’s BorrowPlace::borrow, which Mandry describes as “the first time that we’re actually sort of applying user code post borrow check in this way. It’s all very unsafe.”

With a handle type for MutexGuard that implements BorrowPlace for shared and mutable references, the second render_page would compile exactly as written. The accesses, Mandry says, would “automatically borrow the right place at the right access level for the right amount of time.” In the syntax he proposes, the CRef projection becomes one line:

let field: CRef<'_, Field> = borrow!(s.field);

Once the handle traits are implemented for CRef, Mandry adds, “it just all works with no unsafe except the trait, but in user code there’s no unsafe.”

Pattern matching through smart pointers would become possible with handles. Stable Rust disallows it because “the compiler could evaluate the Deref call more than once while matching and Deref doesn’t promise anything about what it returns.” Each handle is defined to denote the same place on every use. For most existing Deref pointers, Mandry expects authors to make that commitment through a single unsafe marker trait, which his slide calls DerefStable. Nightly Rust has a marker of that kind, DerefPure, and its documentation says the trait’s precise semantics are undecided. He counts exact semantics for a stable version of that trait as one of the challenges still open.

He closes the design section with a picture of current pointer types in three tiers:

1. The built-in pointer types and Box.
2. Library pointers that implement Deref, such as MutexGuard and Rc.
3. Library pointers that cannot implement Deref at all, NonNull and CRef among them.

His goal is to “flatten this hierarchy so that every pointer’s capabilities are a function of its domain, not a function of language limitations.” He credits two people for the design: Benno Lossin, who has driven field projection for years while prototyping in the Linux kernel, and Nadrieril, a language team advisor who contributed its core insight. The design is a prototype, and Mandry asks the community to model their own abstractions in the beyond-refs repository and to report any roadblock they hit. Diagnostics are one area he wants to explore thoroughly next, and one of his slides sets out the standard: “Errors should name the operation in the source code, not an internal trait bound.”

Relocated Trust

Under the proposal, a pointer type’s author writes unsafe trait implementations, and those implementations are the pointer’s entry into Rust’s language of places. The unsafe that a CRef user writes at projection sites now would be written once, in those implementations, where the pointer type’s author makes the promise and reviewers check it. Mandry presents that as the benefit: more complexity for library implementers, in exchange for users who no longer write “behemoths” of unsafe code.

By Rust’s standards that is a real improvement, because the borrow checker would at last receive facts about the places behind library pointers, beyond the lifetime a Deref signature declares. Those facts would remain assertions. A BorrowPlace implementation declares its own access kind and timing, and a DerefStable implementation asserts that repeated calls to deref return a reference to the same place. The compiler would take those declarations as given.

Rust’s standard library is one instance of that arrangement. MutexGuard’s Deref and DerefMut implementations are single unsafe blocks, and its thread safety is an unsafe impl of Sync. As the Rustonomicon says, “Safe Rust inherently has to trust that any Unsafe Rust it touches has been written correctly.”

Interop pointers are the farthest from Rust’s built-in model, and their unsafe trait implementations would make the most assertions. The interop layer resides in unsafe under either design.

Our behavior classification chapter explains why Clef has no unsafe keyword: “each foreign boundary is handled through a structured, checked contract rather than an unchecked region.” Clef code inside that boundary has no raw pointer type. A pointer returned by a C function becomes an opaque CHandle<'T>, whose only use in Clef source is to be passed back to another C binding, and a C function pointer becomes an FnPtr<'F>. Our Clef Compiler Service (CCS) rejects raw address-of expressions and forged handles with diagnostics.

Memory that Clef code reads and writes directly is specified as a region-typed view, Ptr<'T, 'Region, 'Access>, whose type parameters identify the region the memory belongs to and the operations the view admits. Our access kinds correspond to the read-only, write-only and read-write qualifiers of CMSIS, Arm’s microcontroller software interface standard. Clef code accesses memory-mapped registers through the width-specific Mmio handle, which CCS already implements, and Mmio.bind32 selects a register within a named grant that the program’s source declares over memory regions the platform defines. Before lowering, CCS checks that the register lies within the granted region and that the access width matches the hardware transaction. It also checks the register’s and the grant’s permissions for the requested operation.

Facts about the hardware are declarations too: a platform describes its memory spaces with our BAREWire descriptors, written as quotations. The platform bindings chapter specifies how CCS consumes them: they are “read at compile time by CCS, structurally, by type name and field name,” and “the compiler never evaluates the quotation.” CCS turns what it derives from those declarations into obligations on our Program Semantic Graph (PSG), the graph on which the compiler settles a program’s facts before any code is generated. Anything CCS leaves unestablished is either rejected with a diagnostic or, by design, kept as a premise, recorded apart from the evidence the compiler produced. The conformance chapter requires that separation: “Execution-environment hypotheses and dependencies on solvers, kernels, encodings and semantic adapters SHALL be recorded distinctly.”

Mandry’s goal sentence is an apt summary of how our specification assigns capabilities. A view’s capabilities follow from its declared region and access kind, and a register’s follow from the grant that covers it. We give up the variety Mandry credits as Rust’s versatility, because Clef’s boundary vocabulary is a closed set: the four forms named above, from CHandle to Mmio, and the boundary projections the specification admits. We extend that set only by specifying new forms.

Unsettled Semantics

Robert Seacord describes himself as “a C programmer in Rust clothing.” His title at Woven by Toyota is senior staff software engineer, and his books include Effective C and The CERT C Coding Standard. He also mentions that Rust’s language team “has spent a lot of time reviewing my slides.” His premise slide reads: “Rust reduces memory-safety risk, but unsafe Rust remains a language-design and assurance challenge for safety-related systems.”

“Rust has a number of really nice features that C lacks that I would very much like to steal for C, if I could,” Seacord says. Data-race prevention through borrowing rules and the Send/Sync traits is, in his words, “a very, very nice feature of Rust.” He allows that “eventually Rust could well become a safer language than C and C++,” and he places C on the same continuum: “the difference really is one of maturity. In C at least we’ve had 50 years of kind of trying to nail down the undefined behaviors.” His concern is the unsafe subset, which his memory model slide covers in three sentences:

Rust lacks a formal memory model.

Many of the invariants that unsafe operations must uphold are unsettled.

The requirements for unsafe Rust code that ensure that safe Rust is safe and remains safe are unsettled.

He defines undefined behavior in Rust as an operation that “has no valid next state,” and the compiler’s license to assume it never happens is, he says, “exactly the same as C and C++.” He then turns to assurance: “If there is undefined behavior in your Rust program, you can’t even begin to talk about safety or make an assurance case because you can’t say anything about the behavior of that program.” On calls into foreign code, he adds: “You’re calling out to C and, as convener of the C committee, I can tell you that, yeah, C can do whatever.”

In the Rust for Linux figures Seacord presents, unsafe code is densest at that boundary. His slide reports that “Approximately 10% of the Rust kernel code is marked unsafe,” and the share for foundational abstractions is “often much higher (30-50% in specific low-level files) as they must deal with raw hardware and C pointers.” The kernel’s interfaces are C, so “you need an unsafe Rust layer to call these C ABIs to interact with the kernel and then layered on top of that is your safe Rust code.” The slide that diagrams those layers has a single callout: “Unsafe Rust is unavoidable in system programming.”

He considers the obvious remedy, a safe subset of Rust, and his first listed issue is “Eliminating unsafe from Foreign Function Interface (FFI) calls seems improbable.” Most of the others are about certification: a safe subset would require a separate specification and a compiler certified to conform to it, with a coding standard built around the subset.

The specification work he surveys is substantial, and it is proceeding beside a compiler in production:

His summary slide calls this “Work in progress to specify aspects of unsafe Rust behavior with no schedule or overarching plan,” and in the talk he traces the missing schedule to the community effort behind the work: “You can’t get schedules from volunteers.” As things stand, he says, “you’re getting different answers depending on which source you go to,” and “Rust also needs sort of a central authority.”

Our Clef specification and compiler are developed together under one change process, an arrangement that is easy to sustain for a young language with one implementation. The change process opens with “No silent normative change,” and a change counts as complete “only when the specification text, the compiler implementation, and the conformance expectation agree.” Of undefined behavior, Seacord’s central concern, the behavior classification chapter says, “Clef’s defining position is that this class is nearly empty by construction.” Conditions that other language standards leave undefined must be diagnosed as errors under our conformance rules. Where undefined behavior is unavoidable, as in foreign code, the specification “SHALL name it explicitly at the point it arises,” and “a behavior is undefined in Clef only where this specification says so in as many words.”

We take Seacord’s “C can do whatever” as a fact our builds must record. The platform predicates chapter requires hardware documentation and boot mapping assertions to be “recorded separately as external premises,” and it adds that “Assembly and foreign code remain explicit trust boundaries.”

Two of his slides cover uninitialized memory: reading it as a typed value is undefined behavior in Rust. The kernel’s lock-class macro uses MaybeUninit over an Opaque wrapper, and its comment explains why: “Lockdep expects uninit memory when it’s handed a statically allocated struct lock_class_key.” Our specification states that “no value is uninitialised.” Clef is null-free by construction, and CCS rejects the null keyword with diagnostic CCS8010.

Seacord notes on his slide about target architectures that concurrent mutation of adjacent bytes can be undefined behavior and that some targets cannot reliably implement 128-bit integers. He also warns of data races in safe code on targets with relaxed hardware atomics or mismatched ABIs. A target’s stated facts are the principal implementation-defined parameters of our language. CCS analyzes the range of a Clef integer’s values and selects its representation from those the target declares. A known range with no covering representation is a hard coverage error under the width inference chapter, and the numeric selection chapter applies the same rule to reals. We intend to add byte-store atomicity and the atomic orderings each target supports to its stated facts.

Our specification does not contain a formal memory model either. With no unsafe sublanguage, the invariants Seacord calls unsettled are obligations of our compiler and its backends, and we have to bring that young toolchain up to his standard for a safety-related system.

Verdicts at the Boundary

For the narrow family of programs our toolchain compiles end to end today, each buffer handed to the operating system’s write call is the subject of machine-checked obligations. The smallest member of that family is our hello-world sample:

[<EntryPoint>]
let main argv =
    Console.write "Hello, World!"
    Console.writeln ""
    0

CCS derives three obligations from the Console.write call, and the build’s ledger records each with a Common Weakness Enumeration (CWE) tag:

An obligation is a node on our PSG, and the cvc5 SMT solver checks it twice, under the same name, from two separate encodings. The queries are refutations, so unsat means the obligation holds. CCS renders the first query straight from the graph, and Composer, our compiler, runs it again in the compiler’s “middle end”. Lattice, our language server, dispatches those queries to cvc5 as code is written. For the second check, Composer transcribes the obligations into MLIR’s SMT dialect, and the MLIR toolchain’s own exporter turns them back into solver input. The solver has to return unsat again for those obligations, matched by name, before LLVM lowering begins. Both encodings are quantifier-free formulas over linear arithmetic and fixed-width bit-vectors, fragments on which cvc5 is sound and complete.

In the second check, the same propositions are re-encoded on the far side of the staging seam, so a fact lost on its way into MLIR, or altered into one that no longer holds, would fail it. Deriving those facts afresh from the lowered instructions is the translation-validation work we describe in From Proofs to Silicon.

Before Composer publishes a native Linux x86-64 executable, one more check runs in the Rocq proof assitant, formerly named Coq. Composer writes the linked image’s memory map as a Rocq proof file, accounting for every byte of the sections it selects. The map marks its extents as owned by the source program or as trusted foreign bytes. Rocq then checks the compiler’s storage facts against those bytes, including the extent and terminator of every string and the bounds of the buffers handed to write. Print Assumptions reports the lemmas closed, with no added axioms, and Composer moves the binary to its output path only after Rocq accepts the file.

  flowchart TD
    A[CCS derives obligations on our PSG] --> B[cvc5 checks the graph query]
    B --> C[Composer transcribes them to the MLIR SMT dialect]
    C --> D[mlir-translate exports SMT-LIB]
    D --> E[cvc5 checks the exported query]
    E --> F[LLVM lowering and linking]
    F --> G[Composer writes the memory map for Rocq]
    G --> H[Rocq checks storage facts against the bytes]
    H --> I[Composer publishes the binary and its receipt]
    classDef ours fill:#1a2a3a,stroke:#48a,color:#cdf;
    classDef theirs fill:#2a2a2a,stroke:#888,color:#ddd;
    class A,C,G,I ours;
    class B,D,E,F,H theirs;

For the relational properties set out in Between Rocq & A Hard Case, we would check each derivation against a probabilistic rule library proved once in Rocq. A project would enable that check only when its domain warrants that level of proof.

For the hello-world sample, the build receipt pairs each obligation with its machine verdict. It records cvc5 1.3.0 for both solver checks and Rocq 9.1.1 for the memory map, with the exporter taken from LLVM 22.1.8, and it identifies each of those binaries by hash as well as by version. The receipt also lists the six assumptions under which the result holds, two of which contain “declared Linux AMD64 syscall and external runtime behavior” and “foreign extents are byte-accounted” which is to say that there is no export of proofs against syntax - these are proof obligations that are directly engaged in the lowering path.

In the case of an error, it emits a diagnostic that identifies the missing premise: CCS8403, for one, reports that Sys.write requires a proved read-only borrow of the bytes it is handed. The Rocq stage covers data placement and byte extents, and the receipt’s assumptions include “no instruction-level semantic equivalence theorem.” We sketched this direction in Fixing on Falcon as our HelloProof exercise, with proofs at design time, re-checked over the compiler’s intermediates and then re-proved against the binary’s memory map. Seeing it run end to end, against the bytes of the binary itself, is genuinely exciting for us.

At the C boundary, our FFI chapter requires CCS to derive the obligations for each admitted binding during elaboration. An owned acquisition must be paired with its release, cleanup on failure included, and the release retires the caller’s right to use every alias of the handle. A buffer crossing is admitted only with an established byte extent and alignment. For a captured callback, the environment has to outlive its registration and every invocation. We are building that derivation now, and when we checked a native callback fixture on October 3, cvc5 discharged all 62 of its obligations, every one of them numeric. Composer then stopped at the fixture’s function pointers, which it emits only against a target ABI published into the PSG.

Passive Futures

Oxide’s Rain opens “Cancelling Async Rust” with two loops over a channel, both with a timeout added for a debug message. The receiving loop is fine. The sending loop “is often incorrect because not all messages make their way to the channel.” Rain’s case studies are bugs their team found in production at Oxide Computer Company, and Rain speaks as an advocate: “I really love async Rust.”

Rain finds that every option for cancelling synchronous Rust code is “of limited use in some way,” and that synchronous Rust has no universal protocol for cancellation. The first option is a shared flag:

One option is you could have an atomic in some global state which sets a flag saying, I am done with this, I cancel it, and then on the other side you can just check for that flag and you can exit early if that flag is set. This approach works fine for small pieces of code, but it really does not scale well to larger chunks of code because you end up having to sprinkle these checks everywhere and you have to remember to put these checks everywhere. It’s a workable approach, but one that has trouble scaling up.

In Fearless Concurrency Gets Real we described the conventions developers adopt past the edge of the static analysis, and the team that carries them for the maintenance life of the application. Rain’s flag is one of those conventions, here in the words of an engineer who builds production systems in async Rust.

The second option is stranger, and Rain says so: the approach “might seem strange to you,” and “it is strange to me.” Code can cancel work by panicking with a special payload that a frame further up catches. Salsa, the incremental-computation framework under rust-analyzer, cancels this way, and its documentation describes its Cancelled type as “a panic payload indicating that execution of a salsa query was cancelled.” The technique requires panic unwinding, and Rain’s example of a target without it was WebAssembly, where “Rust analyzer currently cannot work with cancellations on Wasm.”

The limit there is the panic strategy of the build. Under panic=abort, the default for Rust’s wasm32-unknown-unknown target, a panic traps and cannot be caught, which matches the situation Rain reported at RustConf 2025. With WebAssembly’s exception-handling proposal, unwinding is possible, and Cloudflare added panic recovery for Rust Workers in April 2026 by building with -Cpanic=unwind on a nightly toolchain that rebuilds the standard library. Whether a framework built this way can cancel work is a function of a build setting and a target, a target dependence like the one Seacord’s architecture slide shows for some of Rust’s guarantees.

Async Rust has one universal protocol in place of those options, and it follows from the property Rain wants the audience to remember: “futures are passive or inert and they are completely inert until awaited or polled.” A future is a state machine in memory, and cancelling it means dropping it, so “any Rust future can be cancelled at any await point.” Rain calls easy cancellation “the greatest strength of async Rust,” and then gives the flip side: it is “far, far too easy.”

In a tree of futures, cancellation of a parent future “propagates down to child futures because of Rust’s single ownership model,” since dropping data drops everything it owns and futures are just data. Reasoning about cancellation, Rain concludes, “becomes this very complicated non-local operation.”

Rain treats cancel safety as a local property: a future is cancel safe if it “can be cancelled without side effects,” as Tokio’s sleep can, while cancelling a channel send loses the message. Cancel correctness, Rain’s own term, is “a global property of system correctness in the face of cancellations.” A cancel-correctness bug, as Rain defines it, has three prongs, all present at once:

1. A cancel-unsafe future exists somewhere in the system.
2. Something actually cancels it.
3. The cancellation violates a property of the system, such as an invariant.

Mandry’s cache sat behind a Mutex, and one of Rain’s production stories from Oxide involves a mutex too. Oxide found that “most uses of mutexes are in order to temporarily violate invariants that are otherwise upheld when a lock isn’t held.” In one production bug, code took per-computer data out of shared state with Option::take and put it back after an action that awaited. A cancellation at that await left the state stuck at None. Oxide now recommends that people “avoid Tokio mutexes entirely.”

Rain’s remedies are patterns, each aimed at one prong:

• A channel send is split into a cancel-safe reserve and an infallible send.
• write_all_buf takes a cursor that records partial progress across a cancellation.
• A future pinned and polled by mutable reference in a select! loop resumes instead of restarting.
• Code that must not be cancelled runs in a task that the runtime drives to completion.

Oxide’s dropshot HTTP server had been dropping request futures whenever a TCP connection closed, so “future cancellations would happen all the way over the network,” and Oxide fixed it by running requests in tasks.

Rain measures the problem against Rust’s central promise: “the whole promise of Rust is that you don’t need to do this kind of non-local reasoning … and future cancellations … fly directly in the face of that and I personally think that they are the least rusty part of Rust.” The language-level fixes on Rain’s list are async drop and linear types, the latter in “unforgettable” and “undroppable” variants. Rain judges that “all of these options have really, really significant challenges.”

Asked whether the problems belong to the language or to libraries such as Tokio, Rain answered that futures are passive because “that is the only way you can write futures in an embedded context,” and that this is “more of a Rust language thing than a library thing.” Asked about actors, Rain recommended them over Tokio mutexes, because “each bit of mutable state is owned by just one task or one actor,” and “overall we found this to be a much more reliable way” of dealing with mutable state.

Visible Delimiters

In our Clef language that passivity is the default for ordinary bindings and arguments. The specification’s expressions chapter reads: “Clef is lazy by default, with call-by-need sharing.” A computation that is bound or passed stays unevaluated until something demands it, and an explicit eager expression demands a value at a stated point. That default is a departure from the strict evaluation of the ML family, toward Haskell’s side of the design space. Lazy<'T> and Cold<'T> values are refinements of that default, and Incremental<'T>, our dependency-tracked form of derived state, is a further refinement with invalidation. The ML lineage of Incremental<'T> is the subject of The Cold Half of Concurrency.

Delimited continuations have been part of our design from the beginning, and the specification defines them as the substrate under every suspension point, an actor’s receive and async { } included. A computation expression is split at its suspension points by the suspension recipe. The expression’s delimiter is the boundary of its block, so the reset is where the block ends, and the structure is settled on the PSG before code exists. Nested delimiters are resolved statically, so “the compiled program contains no prompt tag and performs no dynamic search for a matching reset, on any target.”

Our reading of Salsa’s technique is that a panic with a payload, caught by catch_unwind, is an abortive delimited control operator built from the unwinder and delimited at the catch site, so its availability is a function of the panic strategy. In native Clef, recoverable failures are explicit Result values, and under the specification, compatibility syntax and tooling exceptions “do not imply a native exception-handler stack.” An operation that abandons a computation up to its delimiter would, in our design, be expressed against that delimiter on the PSG.

Resumption is a linear obligation in Clef: a suspended frame is resumed exactly once. A frame silently dropped at a suspension point would violate that obligation. That rule is our starting point for cancellation: an operation on the frame, visible on the PSG, in place of a side effect of dropping it.

Demand withdrawal is the second structure in our cancellation design, and the specification defines much of the machinery behind demand. An Incremental<'T> node that no consumer observes “does not participate in stabilization, even if its inputs are stale,” and demand registration for actor-owned nodes is assigned to Prospero, our supervisor. A subscription is an owner-scoped handle whose release “unsubscribes the observer deterministically,” with no finalizer or garbage collector involved. As specified, retiring an actor disposes of its remaining graph and tears down its effects, and a program calls detach in the rare case of early teardown.

For shared mutable state Rain recommends the actor model, which is also the center of our runtime design. Each actor owns its state, and the specification’s scheduler contract requires a turn to run to completion. In Clef we would give RenderState to a single actor. Its cache would be a persistent Map, where an insertion produces a new version that shares every unchanged subtree, and its template would be an ordinary field of an immutable record. A caller would issue the request-and-reply call renderer.PostAndReply (Render name) to that actor and receive the page in the reply. The handler would read one field and build the next state with the other. Since the turn runs to completion, all access to the state would be serialized without a lock or a guard. CCS would also record the request as a wait-for edge on the PSG, the relation our deadlock analysis is designed to prove acyclic.

Rain’s stuck-at-None bug required a moment when shared state was visibly invalid. In our blog entry on actor behavior, the handler receives the state as a value and returns the next state as a value, so an intermediate condition would exist only inside the handler’s own frame.

Our specification’s closest provision for cancelling a suspended computation covers a synchronous call that the deadlock analysis classifies as unresolved. For that call, the specification requires CCS to elaborate a supervised path that arms a timeout and routes its expiry to the caller’s supervisor. This is part of our “elaboration and saturation” nanopass structure in the Baker component. Composer’s backend, after the Middle End “Alex” component has passively witnessed that structure and lowered it to MLIR, has to realize “the target contract’s scheduling, cancellation and cleanup behavior needed for timeout recovery.” This means that things range depending on whether the target is a CPU, a GPU, NPU, microcontroller or other processor. We are designing the rest from the two structures above: a cancellation bounded by its delimiter, with cleanup ordered by the continuation discipline, and a withdrawal of demand from a dependency graph, made through an operation that has an owner.

Rust’s Strongest Case

We owe Rust’s case full weight: researchers have proved a formal model of the language to be safe for many use cases, and Rust is deployed at increasing scale each year. This steady advance is not an accident.

Modular soundness. Rust’s safety argument is modular: safe code is sound so long as the unsafe code beneath it upholds its invariants. At POPL 2018, Ralf Jung and his co-authors at MPI-SWS and TU Delft published RustBelt, a machine-checked safety proof for a formal model of a realistic subset of Rust. In the RustBelt framework, each library that uses unsafe has a verification condition, and a program is safe if its unsafe code is confined to libraries that satisfy their conditions. They verified ports of standard libraries including Arc, Mutex and RefCell. Along the way they found that MutexGuard<T> was Sync whenever T was merely Send. That soundness bug was in the very type at the center of Mandry’s example, and it was fixed in Rust 1.19.

We differ from Rust on where conditions of this kind are discharged. RustBelt defines what an unsafe library must satisfy, and proving it for a given library is expert work. The Rustonomicon says the standard library’s unsafe code has “generally been rigorously manually checked,” and crate authors rely on review and testing, often under Miri. AWS launched a verification challenge for the standard library with the Rust Foundation as host, and its contributors now check parts of the library’s unsafe code with tools that include model checkers and separation-logic verifiers, against contracts they write. The closest counterparts in Clef are obligations that CCS derives for each program without a contract written in source, and that cvc5 checks on every build. Today those are arithmetic and layout facts, a narrower class than RustBelt’s library conditions.

We leave little to a promise about foreign code. Farscape measures the layout of a C structure from clang for the selected target, and a BAREWire descriptor carries those offsets as evidence. A _Nonnull on a parameter is an obligation on the caller, and CCS establishes it from the type, because a CHandle<'T> is never null. A _Nonnull on a returned pointer is read from clang’s AST of the header, and a checked conversion tests the value the call returned before the handle is admitted. What remains is the library’s behavior past those checks, such as whether the storage behind a handle is still allocated. Our FFI spec entry classifies reliance on that behavior as an external execution hypothesis, recorded in the build’s evidence apart from what the compiler established. A reviewer would then read one list instead of searching the blocks that might assume an annotation holds.

Unsafe beyond interop. In Rust, unsafe code is far more than interop, and Vec and Mutex are both built on it. In Clef there is no unsafe and the equivalent representations, from closures to persistent maps, are specified as compiler-known forms, with proof dispatch to go with it. So the trusted code for them resides in our compiler, CVC5 and Rocq, assuring their integrity. None of these proofs are a developer requirement. They are a coeffect of our Program Semantic Graph and provided “for free” (although the compiler is doing work behind the scenes - no proof work is required by the developer at that level)

Library extensibility. A Rust library author can invent a pointer kind, and under Mandry’s proposal such pointers would be first-class. Our boundary vocabulary is closed by comparison. One C idiom outside it is container_of, which recovers a struct from a pointer to one of its fields. Supporting an idiom like that requires a specification change, a slower path than publishing a crate. We accept that cost deliberately. CCS is designed to check the obligations of each construct in the vocabulary, and it already rejects forged handles and any register access outside its grant. We would rather extend the specification than accept a binding’s declaration as proof.

Deployment evidence. Linux has included Rust support since 6.1 in December 2022, and its maintainers declared the experiment concluded in December 2025. Google counts roughly five million lines of Rust in the Android platform, where memory-safety bugs were under 20 percent of vulnerabilities for the first time in 2025. Windows 11 24H2 includes a Rust implementation of the kernel’s GDI region code. Since November 2017, Firefox has run the Stylo CSS engine, written in Rust. In all four deployments, Rust components run inside a C or C++ system. For us, interop is therefore Rust’s most consequential story, and Mandry’s conference biography lists language interop, with async, as his recent focus at Google.

Programmer recourse. A Rust programmer at the edge of the checker restructures the code, as Mandry does in his fix, or writes unsafe and documents the invariant in a comment. In Clef, the programmer restructures the code or, as our foreign adapters continue to develop, generates a binding adapter in Farscape, itself Clef code that CCS checks. Past that point, the recourse is the specification change described above. As a result, our diagnostics have to identify the missing premise in source terms, as CCS8403 does for an unproved borrow at write, and the conformance chapter states the consequence of falling short: “Silence in place of a required diagnostic is non-conformance.”

A Shared Subtraction

As we recounted in Fearless Concurrency Gets Real, Rust’s first compiler was written in OCaml. That compiler, rustboot, was retired within weeks of self-hosting: by the end of April 2011 the compiler written in Rust was compiling itself, and rustboot was removed from the repository that May. The Rust team dropped the typestate analysis in 2012, and over the next three years they removed the language’s runtime machinery. They abandoned segmented stacks in November 2013, and one reason in an announcement is that a call into C often required a switch to a larger stack. They cut the managed @ pointer from the language in 2014. Under RFC 230 they then removed the green-thread runtime, and the RFC’s motivation lists the setup cost of embedding Rust in C programs. By the 1.0 alpha in January 2015, “Rust no longer has a runtime of any description.”

The team kept the ML core. The Rust Reference credits SML and OCaml for Rust’s algebraic data types and pattern matching. Rust’s type inference has the same source. The removals the team tied to C interop were both runtime pieces: segmented stacks and the green-thread runtime. The OCaml removed in 2011 was the bootstrap compiler’s implementation language.

And it’s worth noting that we made a parallel subtraction from F#, the language Clef descends from. Our specification’s front matter records it: “Constructs that existed solely for interoperation with the .NET Common Language Runtime (CLR), the Base Class Library (BCL), and the managed runtime have been removed.” Like the Rust team, we kept the ML core. The same front matter contrasts F#’s MailboxProcessor, “a library convenience within the .NET ecosystem,” with Clef’s design, in which message-passing concurrency is “a foundational language primitive.” The move away from .NET and the BCL re-intoduced this ML-family language to its systems programming roots.

We diverge from Rust at memory. Rust’s designers put the language’s memory reasoning into the source a programmer writes, from lifetime annotations to unsafe blocks. We placed that reasoning on the graph. As our memory regions specification articulates, “Lifetime verification in Clef is coeffect discipline carried on the Program Semantic Graph, with no ownership or borrowing annotations in the source language.” We diverge again at concurrency. The Rust team removed green threads and later added async and .await to the language in 1.39, with executors supplied by libraries. Rain’s talk is a report from that design. We made delimited continuations and demand-driven evaluation a core element of the language semantics, and our specification defines several forms for continuations over a saved frame, realized per target.

Future Considerations

In viewing these talks we saw confirmation of several ideas for our own boundary, and we think it worth crediting Rust’s work here.

Address stability. Rust has Pin because some memory has to stay where it is, and Mandry’s CRef projections come in pinned versions for C++ objects of that kind. C APIs impose the same condition: a Wayland wl_listener, for one, is linked into a C list by its own address. The boundary obligations in our FFI chapter cover a retained callback environment, which has to outlive its registration and its invocations, a condition on its lifetime alone. Memory registered with foreign code must also keep a fixed address for as long as the registration lasts, and specifying that obligation is next on our list. Our quotation-based Fidelity.Platform libraries carry target information, and will make template resolution and other related considerations part of our FFI implementation.

Aliasing and capability. Our access kinds are capabilities in the CMSIS microcontroller hardware abstraction layer sense, stating which operations a view admits. The access kind that Mandry’s handles declare is an aliasing mode: shared, exclusive or untracked. Both facts matter for foreign memory, since a C++ reference carries “fewer aliasing guarantees” than a Rust reference while Clef code may still need to write through it. We are weighing whether to add an aliasing mode beside our 'Access parameter.

Output cells. No Clef value is uninitialized, and a C out-parameter is uninitialized until the call writes it. In Rust the tool for that case is MaybeUninit, and under Mandry’s proposal a field projected out of a MaybeUninit struct would stay wrapped. Our direction is to keep the output cell inside the binding adapter, out of reach of Clef code, and to admit the written value after the call under the function’s success convention, recorded as a hypothesis about the foreign code. Our marshaling with flat closures (from MLKit) both supplies a concrete anchor point and a location in which our proof boundaries can safely terminate.

Matching on foreign structs. When Clef code matches on a C struct, every read during the match has to target the same place, the commitment Mandry asks of his handles. The projection we are defining for that case requires either a snapshot read into a Clef value or a recorded hypothesis that the place stays stable and unmodified between reads.

An operation checklist. In the Q&A, Mandry put the count for a pointer type at “six or seven or eight different operations,” one of them the discriminant read. We intend to publish a comparable list for native tables, the records with a declared C layout and function-address fields that we are specifying for structures such as wl_listener. Each operation on the list would be either supported with its obligations or rejected with a diagnostic:

Function pointer identity. Seacord’s slide on function pointer identity applies to us as well: a function may be instantiated more than once, and after deduplication, different functions can compare equal. Equality for FnPtr and CHandle values is still an active area of design in Clef. For FnPtr we see two options, rejecting the comparison or giving it a declared-entry meaning. We will settle both questions as we implement native function pointers.

Declared Premises

We are grateful to Tyler Mandry, Robert Seacord and Rain for talks that describe Rust’s hardest edges so precisely. The value we are building toward is a boundary that a reviewer will soon be able to audit by reading its premises. A reviewer would see what our compiler established beside what it assumed about foreign code, and which tool returned each verdict. For a narrow family of programs, our build receipts present that view today. We are extending the same accounting to the C and C++ boundaries now with our Farscape binding generator. And likewise we have designs for cancellation, along with the address and aliasing facts of foreign memory, and will report on them here as the work continues. We take some comfort in that we are able to build these tenets into the Fidelity Framework, both by looking back into ML-family language traditions and the lessons learned from languages like Rust.