alt Hacker NewsMemory safety is absolute table stakes when it comes to formal verification. You can't endow your code with meaningful semantics if you don't have some way of ensuring memory safety.
Replies
foldr • today at 11:16 AM
That's far from trivial in Rust because of 'unsafe' blocks. There are approaches to verifying unsafe code in Rust, but formally verifying a Rust program is still likely to be significantly more complex than formally verifying, say, a Java program.
(And before someone says it: no you don't only have to verify the small amount of code in 'unsafe' blocks. Memory safety errors can be caused by the interaction of safe and unsafe code.)
Indeed, and this is why people who care about this are also proving memory safety in C. The issue is that we do not have good open-source tooling that specifically focuses on formal verification of memory safety in C.