←back to thread

Compiling C to Safe Rust, Formalized

(arxiv.org)
278 points love2read | 5 comments | 20 Dec 24 23:30 UTC | HN request time: 0s | source
Show context
wffurr ◴[21 Dec 24 00:33 UTC] No.42476523[source]▶
Note that this is done for “existing formally verified C codebases” which is a lot different from typical systems C code which is not formally verified.
replies(8): >>42476623 #>>42477360 #>>42478051 #>>42478440 #>>42478560 #>>42478707 #>>42479358 #>>42479797 #
tonetegeatinst ◴[21 Dec 24 03:37 UTC] No.42477360[source]▶
What is the main difference? Can compiler flags force compliance?
replies(3): >>42477457 #>>42477464 #>>42478005 #
immibis ◴[21 Dec 24 07:09 UTC] No.42478005[source]▶
"Formally verified" means someone has written a correct mathematical proof that the code has no bugs (the proof is checked by a computer program to make sure it is correct). This is a very high bar.

I'm not sure what it has to do with translating the code to Rust.

replies(3): >>42478080 #>>42478118 #>>42484000 #
1. swiftcoder ◴[21 Dec 24 07:35 UTC] No.42478080[source]▶
> I'm not sure what it has to do with translating the code to Rust.

Formally verified C programs typically have had all their undefined behaviour already stamped out during the verification process. That makes mapping it over to Rust a lot simpler.

replies(1): >>42478334 #
2. tjoff ◴[21 Dec 24 08:52 UTC] No.42478334[source]▶
Translating undefined behavior is the easy part.
replies(2): >>42479234 #>>42479391 #
3. swiftcoder ◴[21 Dec 24 12:15 UTC] No.42479234[source]▶
Maybe, but only if you know the specifics of the environment in which it is executing (i.e. which compiler/architecture-specific behaviours the code actually relies on)
replies(1): >>42479394 #
4. ◴[21 Dec 24 12:55 UTC] No.42479391[source]▶
5. Filligree ◴[21 Dec 24 12:55 UTC] No.42479394{3}[source]▶
Correctly written C programs don’t have undefined behaviour, so a translator can operate assuming there is none.