Boffins carve up C so code can be converted to Rust

Researchers from Inria and Microsoft present a formalized, semi-automated approach to compile a constrained subset of C ("Mini-C") into memory-safe Rust using the KaRaMeL framework, avoiding unsafe Rust by prohibiting hard-to-translate C features and requiring minimal refactoring; validated on HACL* and EverParse, the method maintained performance while adding safety checks (e.g., fat pointers and bounds checks), and the generated Rust code is already adopted via libcrux in projects like Mozilla NSS and OpenSSH to improve memory safety.