Compiling Rust to readable C with Eurydice
A few years ago, the only way to compile Rust code was using the rustc compiler with LLVM as a backend. Since then, several projects, including
Mutabah’s Rust Compiler (mrustc), GCC’s Rust support (gccrs),
rust_codegen_gcc, and
Cranelift have made enormous progress on diversifying Rust’s compiler implementations. The most recent such project,
Eurydice, has a more ambitious goal: converting Rust code to clean C code. This is especially useful in high-assurance software, where existing verification and compliance tools expect C. Until such tools can be updated to work with Rust, Eurydice could provide a smoother transition for these projects, as well as a stepping-stone for environments that have a C compiler but no working Rust compiler. Eurydice has been used to compile some post-quantum-cryptography routines from Rust to C, for example.
Eurydice was started in 2023, and includes some code under the MIT license and some under the Apache-2.0 license. It’s part of the Aeneas project, which works to develop several different tools related to applying formal verification tools to Rust code. The various
Aeneas projects are maintained by a group of people employed by
Inria (France’s national computer-science-research institution) and Microsoft, but they do accept outside contributions.
Eurydice follows the same general structure as many compilers: take a Rust program, convert it into an intermediate representation (IR), modify the IR with a series of passes, and then output it as code in a lower-level language (in this case, C). Jonathan Protzenko, the most prolific contributor to Eurydice, has
a blog post where he explains the project’s approach. Unlike other compilers, however, Eurydice is concerned with preserving the overall structure of the code while removing constructs that exist in Rust but not in C. For example, consider this Rust function that calculates the least common multiple of two numbers using their greatest common denominator:
Here’s how Eurydice compiles those functions to C:
Whether this C code counts as “readable” is probably a matter of individual taste. It does, however, preserve the structure of the code. Even the evaluation order of the original is preserved by adding extra temporary variables (uu____0 in example_lcm()) where necessary to define an order. (Rust guarantees that if the multiplication overflows and causes a panic, that will happen before any side effects caused by calling example_gcd(), but C only guarantees that if the multiplication is performed in a separate statement.) Compiling the same functions with rustc results in a pair of entangled loops filled with bit-twiddling operations, instead — which is appropriate for machine-code output, but much less readable.
Of course, not all Rust programs can be faithfully represented in C. For example, for loops that use an iterator instead of a range need to be compiled to while loops that call into some of Eurydice’s support code to manage the state of the iterator. More importantly, C has no concept of generics, so Rust code needs to be monomorphized during conversion. This can result in several different implementations of a function that differ only by type — often, the more idiomatic C approach would be to use macros or void * arguments.
The implementation of dynamically sized types also poses certain challenges. In Rust, a structure can be defined where one of its fields does not have a fixed size — like flexible array members in C:
But if that structure is generic, and one of the generic users of the type gives the flexibly sized field a type with a known size, the compiler can take advantage of that knowledge to elide bounds checks where appropriate.
This kind of separation, where some parts of the code may know the size of a type and some may not, is an important semantic detail to preserve in C because of how it interacts with the possibility of formal verification. If Eurydice compiled DynamicallySized to use a flexible array member everywhere, analysis of the C code might point out “missing” bounds checks that were not required in Rust. Conversely, if Eurydice added extra bounds checks, it would need to manufacture extra error paths that don’t appear in the Rust source and that should be completely unused.
So, Eurydice emits two different types: a version of the dynamically sized type that has a flexible array member, and one that has a known-length array member. Converting between the two representations is a no-op at run time, but it technically violates C’s strict-aliasing rule. Therefore Protzenko recommends compiling Eurydice-generated code with -fno-strict-aliasing.
This approach, of compiling a more abstract language to C in a way that preserves the structure of the code, is not new. The
KaRaMeL project, upon which Eurydice is based, does the same thing for the F* programming language. F* is a dependently typed functional programming language used to develop cryptographic libraries. Compiling provably correct F* programs to equivalent C lets those libraries be used in programs where performance is a concern.
Unfortunately, Eurydice doesn’t currently scale much beyond small examples. Rather than implement its own parser and typechecker for Rust code, Eurydice uses another Aeneas tool —
Charon — to extract the parsed and preprocessed program from rustc. When I tested Charon on a variety of Rust packages, it was routinely foiled by more recent Rust features such as
const generics.
When Charon does work, however, it dumps rustc’s medium-level intermediate representation (MIR) as JSON, along with any compiler flags necessary to understand the compilation. Eurydice reads this JSON representation and converts it to KaRaMeL’s intermediate representation. Then it uses a series of small passes over the KaRaMeL code to eliminate some Rust-specific details, before handing things over to the same code-generation logic that KaRaMeL uses for F*.
In its current form, Eurydice works best for small, self-contained programs that avoid complex Rust features. Within that niche, however, it works well. The generated code maintains the same structure as the original Rust code, except for places where Eurydice emits extra intermediate variables or needs some glue code to implement a more complicated feature. On the other hand, small self-contained code is also the easiest to rewrite by hand, so bringing in Eurydice is probably only worthwhile if the original Rust code is going to be updated and one wants an automatic solution to keep them in sync. In any case, Eurydice is only the newest tool in a rapidly expanding collection of ways to fold, spindle, and mutilate Rust code to fit into more environments.
[ Thanks to Henri Sivonen for the topic suggestion. ]
Posted Jan 30, 2026 19:15 UTC (Fri) by Cyberax (✭ supporter ✭, #52523) [Link] (8 responses)
Posted Jan 30, 2026 19:32 UTC (Fri) by comex (subscriber, #71521) [Link] (7 responses)
If you mean bootstrapping by using Eurydice itself as the trusted seed, then that’s theoretically possible (since Eurydice is written in OCaml) but not particularly different from mrustc.
Regardless, if Eurydice is “routinely foiled by more recent Rust features” then it’s nowhere near being able to compile rustc, which uses ~all the features, including many unstable ones.
Posted Jan 30, 2026 20:07 UTC (Fri) by Cyberax (✭ supporter ✭, #52523) [Link] (6 responses)
And more practically, it creates a reasonably static bootstrap chain that allows us to start with just a C compiler.
Posted Jan 30, 2026 23:04 UTC (Fri) by notriddle (subscriber, #130608) [Link] (5 responses)
If your goal is to minimize the number of binary dependencies, then you’re better off using mrustc, which only requires a C++ compiler (which you probably already have as part of your bootstrap chain).
Posted Jan 30, 2026 23:14 UTC (Fri) by Cyberax (✭ supporter ✭, #52523) [Link] (1 responses)
mrustc is indeed another way, but it’s a large complicated C++ code base, with unclear long-term prospects.
Posted Jan 31, 2026 1:11 UTC (Sat) by josh (subscriber, #17465) [Link]
Posted Jan 31, 2026 12:17 UTC (Sat) by ballombe (subscriber, #9523) [Link] (1 responses)
You can run Eurydice on a different machine. Then you only need a C compiler.
Posted Feb 1, 2026 2:02 UTC (Sun) by pabs (subscriber, #43278) [Link]
See also https://bootstrappable.org/ https://lwn.net/Articles/983340/ for some of the philosophy behind this, in short, don’t trust any binaries, even of the Linux kernel etc, and see if you can get a Linux binary starting from scratch. In the bootstrappable.org/live-bootstrap case, they start from a small seed of commented machine code in hex encoding, that you can manually understand and write to a disk, then start the bootstrap.
Posted Feb 1, 2026 1:57 UTC (Sun) by pabs (subscriber, #43278) [Link]
https://github.com/Ekdohibs/camlboot/
Posted Jan 30, 2026 21:58 UTC (Fri) by ballombe (subscriber, #9523) [Link] (3 responses)
Posted Jan 30, 2026 22:54 UTC (Fri) by neggles (subscriber, #153254) [Link]
Posted Jan 30, 2026 23:11 UTC (Fri) by jepsis (subscriber, #130218) [Link] (1 responses)
Yup. It should be something like this:
Or with overflow checks:
Posted Feb 3, 2026 17:03 UTC (Tue) by ttuttle (subscriber, #51118) [Link]
Posted Jan 31, 2026 19:23 UTC (Sat) by SLi (subscriber, #53131) [Link] (5 responses)
If Eurydice is targeting safety critical domains, I’d say this is both true, from a “normal world developer” perspective, and quite irrelevant. C engineered using safety critical standard doesn’t look like “idiomatic C”, and my feeling is that at least the safety standards I’ve dealt with would prefer the way Eurydice does it.
Safety critical processes would likely treat void * as poison to be avoided (likely also heavily restricted) and view macros with extreme suspicion. Avoiding code duplication by what would be seen as “a clever void * trick” would be considered living dangerously and risking lives. If you can have static typing, take static typing, even if it means writing the same routine multiple times. And if you cannot, be prepared to explain why not.
I think people would even argue that monomorphic code is better because it makes it explicit that you have an uint8 path and an uint32 path and allow you to ask if you tested both.
Posted Feb 1, 2026 13:12 UTC (Sun) by mb (subscriber, #50428) [Link]
Posted Feb 2, 2026 21:22 UTC (Mon) by NYKevin (subscriber, #129325) [Link] (3 responses)
It will be very difficult to translate something like the following without monomorphization, so I believe that Eurydice made the right choice regardless of what the safety folks prefer.
CatOrDog is not representable in the C data model. It is, essentially, a compile-time tagged union. That is, it looks and quacks like a tagged union, but the compiler knows which variant is active at compile time, so all other variants disappear during monomorphization, and we emit no code to handle them (the certificates also vanish because they are ZSTs). The post-monomorphization version is trivial to translate into C, because you can just interpret the enum as a newtype around one or the other of its second and third type arguments (as applicable). But the pre-monomorphization version does not live behind a pointer and cannot be trivially represented with void* and such hacks. Note that B and C don’t even need to be the same size or alignment, and Rust can avoid allocating unnecessary space for the larger type if it knows that it is dealing with the smaller type. I don’t believe that there is any reasonable way to accomplish such a thing in C.
Technically, we also need a bit more supporting infrastructure, such as a way to generically construct these enums when the concrete type of A is not visible. Those methods can go into the Animal trait, because its impls can always “see” the concrete type of Self (even when the caller cannot). The unwrap methods demonstrate this visibility. I have elided the othe