←back to thread

Compiling C to Safe Rust, Formalized

(arxiv.org)
291 points love2read | 1 comments | 20 Dec 24 23:30 UTC | HN request time: 0.21s | 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 #
akkad33 ◴[21 Dec 24 10:09 UTC] No.42478707[source]▶
Is Rust formally verified? Not that I know of
replies(3): >>42478873 #>>42480047 #>>42480818 #
PartiallyTyped ◴[21 Dec 24 10:46 UTC] No.42478873[source]▶
You can always run model checkers like Kani, though even that is limited.
replies(1): >>42479351 #
medo-bear ◴[21 Dec 24 12:43 UTC] No.42479351[source]▶
So no?
replies(1): >>42479779 #
johnisgood ◴[21 Dec 24 14:10 UTC] No.42479779[source]▶
The answer is that it is not.

It frustrates me more than it should, I admit, that people always mention Rust when they talk about safety, but never Ada / SPARK. You want formal verification? Use Ada / SPARK. It has been battle-tested. It has been used for critical systems for a really long time now.

(And a compiler being formally verified vs. being able to write formally verified code means two different things.)

replies(3): >>42479874 #>>42484006 #>>42489910 #
1. ◴[22 Dec 24 22:58 UTC] No.42489910[source]▶