Because it takes a lot of effort. Google Frama-C. On the flip side, it can expre... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		PhilipRoman on Dec 21, 2024 \| parent \| context \| favorite \| on: Compiling C to Safe Rust, Formalized 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.

zozbot234 on Dec 21, 2024 [–]

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".

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact