←back to thread

Compiling C to Safe Rust, Formalized

(arxiv.org)
277 points love2read | 1 comments | 20 Dec 24 23:30 UTC | HN request time: 0.25s | source
Show context
alkonaut ◴[21 Dec 24 09:35 UTC] No.42478567[source]▶
If you used a naïve translation to Rust, wouldn’t you get parts that are safe and parts that are unsafe? So your manual job would need to be only verifying safety in the unsafe regions (same as when writing rust to begin with)?

Seems it would be a win even if the unsafe portion is quite large. Obviously not of it’s 90% of the end result.

replies(2): >>42479369 #>>42481284 #
1. CodesInChaos ◴[21 Dec 24 12:49 UTC] No.42479369[source]▶
A naïve translation would produce rust code which is almost entirely unsafe (using raw pointers instead of references everywhere). Translating to references is difficult, since C code isn't written with the restrictions of the Rust alias model / borrow-checker in mind.