←back to thread

Compiling C to Safe Rust, Formalized

(arxiv.org)
278 points love2read | 2 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 #
1. LPisGood ◴[21 Dec 24 04:02 UTC] No.42477464[source]▶
My understanding is that formal verification is a tough goal to achieve and that it usually requires designing the program or the language to be a specific way.

The problem with transpiling C to rust is that unsafe and unverified behavior can be a key property of the behavior resulting program, so there isn’t an obvious way to spit out a sort of rustified (CRustified?) binary that matches the behavior of the C program.

replies(1): >>42477806 #
2. thunkingdeep ◴[21 Dec 24 05:55 UTC] No.42477806[source]▶
Typical term is “Oxidized”. I think they feel clever when they do the RiiR thing and say that.