(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 #

jokoon ◴[21 Dec 24 09:13 UTC] No.42478440[source]▶

>>42476523 #

What is formally verified C? Why isn't there more of it?

replies(1): >>42478626 #

PhilipRoman ◴[21 Dec 24 09:48 UTC] No.42478626[source]▶

>>42478440 #

Because it takes a lot of effort. Google Frama-C. On the flip side, it can express not just memory safety constraints, but also correctness proofs.

In this case it's not about Frama-C or similar tools though, see your sibling comments about the caveats.

replies(1): >>42478689 #

1. zozbot234 ◴[21 Dec 24 10:05 UTC] No.42478689[source]▶

>>42478626 #

Arguably, generating verified C from a low-level focused subset of F* (Low*, used in the HACL project) is close enough to count as a "similar tool".

↑

Compiling C to Safe Rust, Formalized