Compiling C to Safe Rust, Formalized

Original Article ↗ Hacker News Discussion ↗

Researchers are exploring how to translate C-like, formally verified code into memory-safe Rust, with the ambitious goal of preserving both performance and safety guarantees. Commenters largely agree this is valuable for high-assurance libraries (e.g., cryptography and parsers), but point out major caveats: the current work targets a small, well-behaved subset of C generated from the F* language, may reject many real-world patterns, and can still introduce panics or behavior changes. The thread situates this effort among other tools (like C2Rust and formal analyzers for C), debates whether wholesale conversion is worthwhile compared to hardening existing C, and highlights the broader tension between research prototypes, marketing claims, and what is practical for large legacy codebases.

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.