Compiling C to Safe Rust, Formalized

Scope and Claims of the Paper

• Many commenters note the work targets a very restricted, well-behaved subset of C, largely code generated from F* (HACL*), not arbitrary industrial C.
• Several argue the title (“Compiling C to Safe Rust, Formalized”) is misleading: it’s closer to “subset of F* to partially safe Rust” than general C→Rust.
• Others defend this as normal academic scoping: a research step in a large design space, not a product claiming to “solve C→Rust.”
• The author clarifies: it’s an academic paper, exploring what is required to get safe Rust from C-like code, accepting errors/aborts and a constrained subset, with plans for a real C frontend.

Technical Challenges in C→Safe Rust

• Core difficulty: mapping C’s free-form pointer/aliasing patterns into Rust’s ownership and borrow rules.
• Example discussed: a C pointer alias to a stack array becomes a boxed copy in Rust; this can silently change semantics unless the tool rejects such cases.
• The paper’s approach will error out on patterns where aliasing and reliance on the original object cannot be safely preserved; this may induce many conservative false negatives.
• Translating pointer arithmetic into Rust slices is seen as a major positive step; previous tools often fell back to unsafe raw pointers.
• Some argue that for many real C designs (e.g., complex or custom linked lists, unsafe string APIs, JITs) preserving exact behavior without pervasive unsafe is impossible.

Formal Verification Context

• “Formally verified C” here means C code with mathematically proven properties against a spec; such code typically already avoids undefined behavior and follows a restrictive style.
• Verified C eases translation to Rust because many dangerous patterns have been stamped out.
• Several point out limits: specifications can be buggy; formal verification validates the model, not the “real world.”

Rust Safety, Alternatives, and Tooling

• Rust itself is not fully formally verified; only subsets (e.g., borrow checker models) and parts of the standard library have formal proofs.
• Debate over Rust “hype”: it greatly improves memory safety vs C/C++, but doesn’t guarantee full correctness and still uses unsafe internally.
• Alternatives like Ada/SPARK and heavy-weight C verification tools (Frama-C, Astree, RV-Match, CompCert, Softbound+CETS) are mentioned as existing paths to safety.
• Some suggest that improving C verification and generating safer C/wrappers may be more directly useful than full translation, but others argue that safe Rust remains a stronger long-term foundation.