Eurydice compila Rust a C legible para verificación formal
Compiling Rust to readable C with Eurydice
Eurydice, parte del proyecto Aeneas, convierte código Rust en C limpio preservando su estructura, a diferencia de rustc que genera bucles enrevesados. Esto facilita la verificación formal y la transición en entornos de alta seguridad que solo aceptan C. Aunque aún no escala más allá de programas pequeños, ya se ha usado para criptografía post-cuántica.
Si Eurydice compilara DynamicallySized para usar un miembro de array flexible en todas partes, el análisis del código C podría señalar comprobaciones de límites 'faltantes' que no eran necesarias en Rust.
- chias
Qué elección de nombre de producto tan excelente :D
"You're da C"
- Neywiny
Ojalá esto cubriera más características específicas de Rust que lo hacen más seguro en tiempo de ejecución, no solo más seguro en tiempo de compilación. Supongo que para cuando llega al IR es lo mismo, pero sería bonito verlo subir de nuevo a C. Como la comprobación de límites.
- fithisux
D y C++ se beneficiarían de algo como esto.