←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: 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 #
akkad33 ◴[21 Dec 24 10:09 UTC] No.42478707[source]▶
Is Rust formally verified? Not that I know of
replies(3): >>42478873 #>>42480047 #>>42480818 #
antiquark ◴[21 Dec 24 17:11 UTC] No.42480818[source]▶
Rust doesn't have a specification or standard yet, which would make it difficult to formally verify.

https://stackoverflow.com/questions/75743030/is-there-a-spec...

replies(1): >>42480860 #
1. gpm ◴[21 Dec 24 17:16 UTC] No.42480860{3}[source]▶
It does have a specification: https://github.com/ferrocene/specification

It also strikes me as extraordinarily unlikely that any formal verification effort will use the existing specification, and not build their own (using their own formal language) as they go.