Hacker News new | past | comments | ask | show | jobs | submit

Compiling C to Safe Rust, Formalized

https://arxiv.org/abs/2412.15042
loading story #42476523
loading story #42478558
loading story #42478567
loading story #42476714
loading story #42477991
loading story #42478433
loading story #42478644
loading story #42476729
loading story #42476421
loading story #42478818
loading story #42477506
loading story #42476456
Ugh. They didn't compile any C to Rust. They modified the F*-to-C compiler to emit Rust instead. So they compiled F* to safe Rust. And they couldn't even do that 100% reliably; some valid F* constructs couldn't be translated into Rust properly. They could either translate it into Rust code that wouldn't compile, or translate it into similar-looking Rust code that would compile, but would produce incorrect results.

Flagged, this is just a lie of a title.

loading story #42477522
loading story #42476430
loading story #42477322