arxiv: 2604.17261 · v2 · submitted 2026-04-19 · 💻 cs.PL

Recognition: unknown

&inator: Correct, Precise C-to-Rust Interface Translation

Ayden Coughlin, Michael D. Bond, Victor Chen

Authors on Pith no claims yet

Pith reviewed 2026-05-10 06:01 UTC · model grok-4.3

classification 💻 cs.PL

keywords C-to-Rust translationinterface translationborrow checkingconstraint solvingsemantic equivalencesafe Rustownership

0 comments

The pith

&inator produces the first correct and precise Rust interfaces for C top-level declarations using constraint solving on equivalence and borrow rules.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents &inator as a method to translate C structs and function signatures into Rust declarations. It formulates the problem as constraints that enforce semantic equivalence to the original C code while satisfying Rust ownership and borrowing discipline. If solved, the output interface admits an implementation in safe Rust that preserves behavior and uses the simplest possible types. This matters for incremental migration of system software because it supports modular translation without whole-program unsafe blocks at the boundary. Results on real C programs confirm it works in practice though some features and scale remain open.

Core claim

&inator employs a novel constraint-based formulation of semantic equivalence and type correctness including borrow-checking rules to produce a Rust interface that is correct (admits a semantics-preserving implementation in safe Rust) and precise (uses the simplest, least costly types).

What carries the argument

Constraint-based formulation of semantic equivalence and borrow-checking rules applied to C top-level declarations

If this is right

C programs can expose top-level interfaces that Rust code can call without unsafe blocks while preserving original semantics.
Interface translation becomes a reliable first step toward whole-program C-to-Rust migration.
Borrow-checking constraints can be solved alongside equivalence constraints rather than checked after translation.
Precision in type choice reduces runtime overhead compared with overly conservative Rust wrappers.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same constraint approach could extend to translating C function bodies once interfaces are fixed.
If scaling improves, it might support automated migration of large codebases like operating systems or libraries.
Similar constraint formulations could apply to other language pairs with ownership models, such as C to Go or C++ to Rust.

Load-bearing premise

The constraint system encoding semantic equivalence and Rust borrow rules can be solved efficiently and completely for real C top-level declarations without manual workarounds for unsupported features.

What would settle it

A real C program whose &inator-generated Rust interface either requires unsafe code to implement a semantics-preserving version or uses strictly more expensive types than a manual safe-Rust equivalent.

Figures

Figures reproduced from arXiv: 2604.17261 by Ayden Coughlin, Michael D. Bond, Victor Chen.

**Figure 2.** Figure 2: An example C program and translated Rust interface. The Rust interface shows grayed-out Rust [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗

**Figure 3.** Figure 3: &inator performs interface translation (see [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗

**Figure 4.** Figure 4: Context-free grammar for the source language of & [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗

**Figure 5.** Figure 5: A program snippet in the source language of & [PITH_FULL_IMAGE:figures/full_fig_p008_5.png] view at source ↗

**Figure 6.** Figure 6: Grammar for Rust type fragments (RTypeFrag) [PITH_FULL_IMAGE:figures/full_fig_p009_6.png] view at source ↗

**Figure 7.** Figure 7: The program from [PITH_FULL_IMAGE:figures/full_fig_p010_7.png] view at source ↗

**Figure 8.** Figure 8: Pointer transformations considered by &inator. Each node is a set of Rust type fragments, where 𝜇 ∈ Qual and 𝑅 ∈ {shared, mut}. Each edge from 𝑇1 to 𝑇2 is labeled with a Rust expression that transforms a pointer 𝑝 of type 𝑇1 to a pointer of type 𝑇2. Expressions on dashed edges invalidate 𝑝, while expressions on solid edges do not. 𝑇1 is transformable (§7.6) to 𝑇2 if 𝑇2 is reachable from 𝑇1 by traversing an… view at source ↗

read the original abstract

Automatically translating system software from C to Rust is an appealing but challenging problem, as it requires whole-program reasoning to satisfy Rust's ownership and borrowing discipline. A key enabling step in whole-program translation is interface translation, which produces Rust declarations for the C program's top-level declarations (i.e., structs and function signatures), enabling modular and incremental code translation. This paper introduces correct, precise C-to-Rust interface translation, called &inator. &inator employs a novel constraint-based formulation of semantic equivalence and type correctness including borrow-checking rules to produce a Rust interface that is correct (i.e., the interface admits a semantics-preserving implementation in safe Rust) and precise (i.e., it uses the simplest, least costly types). Our results show &inator produces correct, precise Rust interfaces for real C programs, but support for certain C features and scaling to large programs are challenges left for future work. This work advances the state of the art by being the first correct, precise approach to C-to-Rust interface translation.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a constraint-based formulation for C-to-Rust interfaces that tries to bake in borrow rules up front, but the evaluation details are too thin to back the strong claims.

read the letter

The core idea is a constraint solver that encodes semantic equivalence plus Rust's borrow-checking rules to turn C top-level declarations into Rust interfaces. The goal is interfaces that are correct (they allow a semantics-preserving safe-Rust implementation) and precise (they pick the simplest possible types). That formulation is the main new piece; earlier work either produced unsafe interfaces or applied fixes after translation. The approach is worth looking at because interface translation really is a bottleneck for incremental C-to-Rust migration of systems code. If the solver can be made to terminate and produce usable results on typical C programs, it would be a practical step forward. The abstract says the tool was run on real C programs and produced correct interfaces, which is the right kind of claim to make. The stress-test note is fair: the paper itself lists support for certain C features and scaling to large programs as open challenges. That means the solver either fails or requires manual workarounds on programs that hit those limits, so the “first correct and precise” framing only holds inside the supported subset. There are no numbers on how many programs were tested, what their sizes were, or how correctness was actually verified beyond the abstract statement. Without those details it is hard to judge whether the method scales or generalizes. The paper is aimed at researchers working on language migration and safe systems software. Someone already thinking about C-to-Rust tools would get value from the constraint encoding even if they end up re-implementing parts of it. It deserves a serious referee round because the problem is real and the formulation is a clear departure from post-hoc fixes, but the referees will need to see concrete evaluation data and a clearer statement of the supported C subset before the main claims can be accepted.

Referee Report

2 major / 0 minor

Summary. The paper introduces &inator, a system for C-to-Rust interface translation that uses a novel constraint-based encoding of semantic equivalence and Rust borrow-checking rules to generate correct (admitting semantics-preserving safe-Rust implementations) and precise (using simplest types) Rust declarations for C top-level structs and function signatures. It claims this is the first such correct and precise approach and reports that &inator produces such interfaces for real C programs, while noting that support for certain C features and scaling to large programs remain future work.

Significance. If the central claim holds, the work would be significant for enabling modular, incremental C-to-Rust translation by solving a key whole-program reasoning challenge via constraints rather than ad-hoc rules. The constraint formulation of borrow rules and semantic equivalence is a technical contribution that could generalize beyond interfaces. However, the absence of any evaluation details (methodology, test cases, verification) in the abstract and the explicit future-work caveats on features and scale limit the assessed impact.

major comments (2)

[Abstract] Abstract: the claim that 'results show &inator produces correct, precise Rust interfaces for real C programs' is unsupported because the abstract (and provided text) gives no description of evaluation methodology, specific C programs tested, how correctness was verified (e.g., via manual inspection, compilation checks, or semantic equivalence tests), or how precision was measured. This directly undermines the 'first correct' claim and the weakest assumption that the solver works completely and automatically.
[Abstract] Abstract: the paper states that 'support for certain C features and scaling to large programs are challenges left for future work' immediately after claiming production of correct interfaces for real programs. This indicates that the constraint solver either fails to terminate, produces incomplete results, or requires manual adjustments on programs containing those features, contradicting the central claim that the encoding 'can be solved efficiently and completely for the top-level declarations of real-world C programs without requiring manual adjustments.'

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive review and for highlighting areas where the abstract could better support our claims. We agree that revisions are needed and will update the abstract to include a concise description of the evaluation and to clarify the scope of our results. We respond to each major comment below.

read point-by-point responses

Referee: [Abstract] Abstract: the claim that 'results show &inator produces correct, precise Rust interfaces for real C programs' is unsupported because the abstract (and provided text) gives no description of evaluation methodology, specific C programs tested, how correctness was verified (e.g., via manual inspection, compilation checks, or semantic equivalence tests), or how precision was measured. This directly undermines the 'first correct' claim and the weakest assumption that the solver works completely and automatically.

Authors: We acknowledge that the abstract does not contain sufficient evaluation details. The full manuscript includes a dedicated evaluation section that specifies the methodology, the real C programs tested, verification of correctness via compilation and manual semantic review, and precision assessment through type comparison. We will revise the abstract to summarize these elements briefly, including the scope of programs evaluated, to substantiate the results and the 'first correct' claim. revision: yes
Referee: [Abstract] Abstract: the paper states that 'support for certain C features and scaling to large programs are challenges left for future work' immediately after claiming production of correct interfaces for real programs. This indicates that the constraint solver either fails to terminate, produces incomplete results, or requires manual adjustments on programs containing those features, contradicting the central claim that the encoding 'can be solved efficiently and completely for the top-level declarations of real-world C programs without requiring manual adjustments.'

Authors: The reported results apply to real C programs using only the C features supported in the current implementation of &inator. The future-work statement addresses extensions to additional features and larger scales. For the evaluated programs, the solver produces complete, automatic results without manual adjustments. We will revise the abstract to explicitly note that results are for the supported feature subset and to distinguish this from planned extensions. revision: yes

Circularity Check

0 steps flagged

No circularity in algorithmic formulation or claims

full rationale

The paper describes a novel constraint-based algorithm for producing correct and precise Rust interfaces from C top-level declarations. The central claims rest on the explicit formulation of semantic equivalence plus borrow-checking rules, followed by evaluation against external real-world C programs. No equations, predictions, or first-principles results reduce to their own inputs by construction. There are no self-definitional steps, fitted inputs renamed as predictions, load-bearing self-citations, uniqueness theorems imported from the authors' prior work, or ansatzes smuggled via citation. The approach is presented as self-contained and externally evaluated; mentions of unsupported features and scaling challenges are acknowledged as future work rather than hidden assumptions that collapse the derivation. This is the normal case of an algorithmic systems paper whose correctness argument does not tautologically presuppose its own outputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard semantics of C and Rust plus the assumption that constraint solving can capture borrow-checking rules without additional ad-hoc rules.

axioms (2)

domain assumption Rust ownership and borrowing discipline must be satisfied for any semantics-preserving safe-Rust implementation
Invoked as the basis for the constraint formulation of type correctness.
domain assumption Semantic equivalence between C and Rust interfaces can be expressed as a solvable constraint system
Core modeling choice stated in the abstract.

pith-pipeline@v0.9.0 · 5473 in / 1170 out tokens · 46225 ms · 2026-05-10T06:01:03.798885+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

33 extracted references · 18 canonical work pages

[1]

Victor Chen, Ayden Coughlin, and Michael D. Bond. 2026.&inator artifact. doi:10.5281/zenodo.19650358

work page doi:10.5281/zenodo.19650358 2026
[2]

DARPA. 2025. TRACTOR: Translating All C to Rust. https://www.darpa.mil/research/programs/translating-all-c-to- rust

2025
[3]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. InProceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems(Budapest, Hungary)(TACAS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg, 337–340

2008
[4]

Edwards and Chun Li

Stephen A. Edwards and Chun Li. 2004.Determining Interfaces using Type Inference. Technical Report CUCS- 052-04. Columbia University, Department of Computer Science. https://www.cs.columbia.edu/~sedwards/papers/ edwards2004determining.pdf

2004
[5]

Mehmet Emre, Peter Boyland, Aesha Parekh, Ryan Schroeder, Kyle Dewey, and Ben Hardekopf. 2023. Aliasing Limits on Translating C to Safe Rust.Proc. ACM Program. Lang.7, OOPSLA1, Article 94 (April 2023), 29 pages. doi:10.1145/3586046

work page doi:10.1145/3586046 2023
[6]

Mehmet Emre, Ryan Schroeder, Kyle Dewey, and Ben Hardekopf. 2021. Translating C to safer Rust.Proc. ACM Program. Lang.5, OOPSLA, Article 121 (Oct. 2021), 29 pages. doi:10.1145/3485498

work page doi:10.1145/3485498 2021
[7]

Manuel Fahndrich and Robert DeLine. 2002. Adoption and focus: practical linear types for imperative programming. InProceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation(Berlin, Germany)(PLDI ’02). Association for Computing Machinery, New York, NY, USA, 13–24. doi:10.1145/512529.512532

work page doi:10.1145/512529.512532 2002
[8]

Aymeric Fromherz and Jonathan Protzenko. 2026. Scylla: Translating an Applicative Subset of C to Safe Rust.Proc. ACM Program. Lang.10, OOPSLA1, Article 121 (April 2026), 27 pages. doi:10.1145/3798229

work page doi:10.1145/3798229 2026
[9]

Galois and Immunant. 2025. C2Rust: Migrate C code to Rust. https://github.com/immunant/c2rust

2025
[10]

Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. 2002. Region-Based Memory Management in Cyclone. InProceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation(Berlin, Germany)(PLDI ’02). Association for Computing Machinery, New York, NY, USA, 282–293. doi:10.1145/512529.512563

work page doi:10.1145/512529.512563 2002
[11]

Jaemin Hong and Sukyoung Ryu. 2024. Type-migrating C-to-Rust translation using a large language model.Empirical Softw. Engg.30, 1 (Oct. 2024), 38 pages. doi:10.1007/s10664-024-10573-2

work page doi:10.1007/s10664-024-10573-2 2024
[12]

Anirudh Khatry, Robert Zhang, Jia Pan, Ziteng Wang, Qiaochu Chen, Greg Durrett, and Isil Dillig. 2025. CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation. arXiv:2504.15254 [cs.SE] https://arxiv.org/abs/2504.15254

work page arXiv 2025
[13]

2022.Cost of Poor Software Quality in the US: A 2022 Report

Herb Krasner. 2022.Cost of Poor Software Quality in the US: A 2022 Report. Technical Report. Consortium for Information & Software Quality. https://www.it-cisq.org/the-cost-of-poor-quality-software-in-the-us-a-2022-report/

2022
[14]

Chris Lattner and Vikram Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transfor- mation. InProceedings of the International Symposium on Code Generation and Optimization: Feedback-Directed and Runtime Optimization(Palo Alto, California)(CGO ’04). IEEE Computer Society, USA, 75

2004
[15]

Ruishi Li, Bo Wang, Tianyu Li, Prateek Saxena, and Ashish Kundu. 2025. Translating C To Rust: Lessons from a User Study. InNetwork and Distributed System Security (NDSS) Symposium. doi:10.14722/ndss.2025.241407

work page doi:10.14722/ndss.2025.241407 2025
[16]

Cordy, and Ahmed E

Michael Ling, Yijun Yu, Haitao Wu, Yuan Wang, James R. Cordy, and Ahmed E. Hassan. 2022. In Rust We Trust: A Transpiler from Unsafe C to Safer Rust. InProceedings of the ACM/IEEE 44th International Conference on Software Engineering: Companion Proceedings(Pittsburgh, Pennsylvania)(ICSE ’22). Association for Computing Machinery, New York, NY, USA, 354–355....

work page doi:10.1145/3510454.3528640 2022
[17]

Aravind Machiry, John Kastner, Matt McCutchen, Aaron Eline, Kyle Headley, and Michael Hicks. 2022. C to checked C by 3C.Proc. ACM Program. Lang.6, OOPSLA1, Article 78 (April 2022), 29 pages. doi:10.1145/3527322 15https://github.com/PLaSSticity/refinator-impl Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 192. Publication date: June 2026. 192:24 Vict...

work page doi:10.1145/3527322 2022
[18]

Niels Mündler, Jingxuan He, Hao Wang, Koushik Sen, Dawn Song, and Martin Vechev. 2025. Type-Constrained Code Generation with Language Models.Proc. ACM Program. Lang.9, PLDI, Article 171 (June 2025), 26 pages. doi:10.1145/3729274

work page doi:10.1145/3729274 2025
[19]

Necula, Scott McPeak, and Westley Weimer

George C. Necula, Scott McPeak, and Westley Weimer. 2002. CCured: Type-Safe Retrofitting of Legacy Code. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Portland, Oregon) (POPL ’02). Association for Computing Machinery, New York, NY, USA, 128–139. doi:10.1145/503272.503286

work page doi:10.1145/503272.503286 2002
[20]

Lily Hay Newman. 2022. The ‘Viral’ Secure Programming Language That’s Taking Over Tech. https://www.wired. com/story/rust-secure-programming-language-memory-safe

2022
[21]

Vikram Nitin, Rahul Krishna, Luiz Lemos do Valle, and Baishakhi Ray. 2025. C2SaferRust: Transforming C Projects into Safer Rust with NeuroSymbolic Techniques. arXiv:2501.14257 [cs.SE] https://arxiv.org/abs/2501.14257

work page arXiv 2025
[22]

https://rust-lang.github.io/rfcs/2094-nll.html

Non-Lexical Lifetimes RFC 2017. https://rust-lang.github.io/rfcs/2094-nll.html

2017
[23]

https://github.com/rust-lang/polonius

Polonius 2025. https://github.com/rust-lang/polonius

2025
[24]

https://rustc-dev-guide.rust-lang.org/about-this-guide.html

Rust Compiler Development Guide 2025. https://rustc-dev-guide.rust-lang.org/about-this-guide.html

2025
[25]

Biruk Tadesse, Vikram Nitin, Mazin Salah, Baishakhi Ray, Marcelo d’Amorim, and Wesley Assunção. 2026. Code Quality Analysis of Translations from C to Rust. arXiv:2602.00840 [cs.SE] https://arxiv.org/abs/2602.00840

work page arXiv 2026
[26]

https://doc.rust-lang.org/stable/reference/

The Rust Reference 2025. https://doc.rust-lang.org/stable/reference/

2025
[27]

https://doc.rust-lang.org/std/

The Rust Standard Library Documentation 2025. https://doc.rust-lang.org/std/

2025
[28]

The White House. 2024. Fact Sheet: ONCD Report Calls for Adoption of Memory Safe Programming Languages and Addressing the Hard Research Problem of Software Measurability. https://bidenwhitehouse.archives.gov/oncd/briefing- room/2024/02/26/memory-safety-fact-sheet

2024
[29]

Hanliang Zhang, Cristina David, Meng Wang, Brandon Paulsen, and Daniel Kroening. 2025. Scalable, Validated Code Translation of Entire Projects using Large Language Models.Proc. ACM Program. Lang.9, PLDI, Article 212 (June 2025), 26 pages. doi:10.1145/3729315

work page doi:10.1145/3729315 2025
[30]

Hanliang Zhang, Cristina David, Yijun Yu, and Meng Wang. 2023. Ownership Guided C to Rust Translation. In Computer Aided Verification: 35th International Conference, CA V 2023, Paris, France, July 17–22, 2023, Proceedings, Part III(Paris, France). Springer-Verlag, Berlin, Heidelberg, 459–482. doi:10.1007/978-3-031-37709-9_22

work page doi:10.1007/978-3-031-37709-9_22 2023
[31]

Tianyang Zhou, Haowen Lin, Somesh Jha, Mihai Christodorescu, Kirill Levchenko, and Varun Chandrasekaran
[32]

Llm-driven multi-step translation from c to rust using static analysis.arXiv preprint arXiv:2503.12511, 2025

LLM-Driven Multi-step Translation from C to Rust using Static Analysis. arXiv:2503.12511 [cs.SE] https: //arxiv.org/abs/2503.12511 Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 192. Publication date: June 2026. &inator: Correct, Precise C-to-Rust Interface Translation 192:25 A Definitions and Notation This section defines definitions and notation u...

work page arXiv 2026
[33]

ACM Program

∋𝑡 ′ 2 ⇒LT(𝑡 1) ⊇LT(𝑡 2) Proc. ACM Program. Lang., Vol. 10, No. PLDI, Article 192. Publication date: June 2026. &inator: Correct, Precise C-to-Rust Interface Translation 192:35 D.2 In-Scope Loans Here, we show the constraints that §9.2 introduced. &inator’s constraints represent the in-scope loans at each program point in the SMT function defined as follo...

2026