4 ms·
What is formally verified C? Why isn't there more of it?
by jokoon 2y ago
What is formally verified C? Why isn't there more of it?
- PhilipRoman 2y agoBecause 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 2y agoArguably, 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".