←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.209s | 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. nickpsecurity ◴[21 Dec 24 03:59 UTC] No.42477457[source]▶
Formal verification often requires simplified code in a restrictive style. You might not even be able to use C features or structures that have the performance you want. How theorem provers and brains work are also different enough that making something easy for one often makes it harder for the other.

You can also see this effect in the article on the history of Coverity’s analyzer. Real-world code was horrible to deal with vs the academic examples they started with.

https://cacm.acm.org/research/a-few-billion-lines-of-code-la...