←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: 0.646s | 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 #
medo-bear ◴[21 Dec 24 12:45 UTC] No.42479358[source]▶
What is the benefit of compiling formally correct code to Rust? It seems that all the possible benefits are already there (if not more)
replies(1): >>42480064 #
1. gpm ◴[21 Dec 24 15:01 UTC] No.42480064[source]▶
I suppose hypothetically putting it in an easier language to make changes in. Though it's hard to imagine it being easier to make changes to transpiled code than the original.

Alternatively this might be seen as a stepping stone to translating non-formally-verified C to rust, which I understand the US government has expressed a fair bit of interest in.

replies(1): >>42480100 #
2. medo-bear ◴[21 Dec 24 15:09 UTC] No.42480100[source]▶
Good luck with both of that. Otherwise people whose dayjob is rewritting everything in Rust will soon be out of a job