Hacker News new | past | comments | ask | show | jobs | submit login

> Both manual and automated proof with separation logic has a lot more automation since then. Yet, I think programmers will more easily learn to intuitively and heuristically structure their programs to pass Rust's automated, formal checker than learning expert-level C, separation logic, and/or formal proof.

Yeah but aren't these formal proof methods a lot more general, and thus more widely applicable? In other words, does Rust provide the right balance between security and complexity?




Rust has what we often call a "lightweight" formal method. These are those with simpler types of specification and/or more automated use. They tend to be quite specialized since that improves automation. The limited properties it proves are why it's so much easier to use than the general methods.

Also note that the problems the borrow checker handles are really hard to do safely in general without overhead. They're hard to test for and debug, too. So, the use of a limited logic with automation just for that makes sense. It's why the other tools for C code were developed, too. Before that, people were using things like SPIN model checker for such things. Again, that looks like overkill to get just a few safety properties vs Rust's built-in method that's simpler.




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

Search: