←back to thread

Compiling C to Safe Rust, Formalized

(arxiv.org)
278 points love2read | 1 comments | 20 Dec 24 23:30 UTC | HN request time: 0.202s | 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. SAI_Peregrinus ◴[22 Dec 24 02:28 UTC] No.42484000[source]▶
> "Formally verified" means someone has written a correct mathematical proof that the code has no bugs

No, only that it complies with a formal specification. The code will have bugs if and only if the specification has bugs.

The difficulty of writing a bug-free formal specification is just as great as writing bug-free code. In some domains it's easier to write the specification, but not in most. Fully specifying what a program shoud do is often the hardest part of programming, after all.