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

Wait until you see what it took to do one in C with the formally-checked, safety guarantees of Rust around the time Rust was being developed:

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.553...

https://ac.els-cdn.com/S0167642313000191/1-s2.0-S01676423130...

Ok, so author needed to know C extremely well (i.e. "language lawyer"), comfortable with separation logic, able to turn informal requirements into specifications, use of ghost code, and have a SMT solver. The solvers often fail on some stuff that requires formal proof by rare experts. However, that expert was able to automatically verify a singly-linked list with just 113 ghost statements for the 90 statements in C. That's more specs than code! Industrial case studies in other article give more examples. More importantly, when making the C code as verifiably safe as Rust, the effort required had developers cranking it out at rate of two lines of code per hour.

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. And Rust can still do reference counting or unsafe operation in event it can't check something.

This write-up you all keep linking doesn't prove what you think it proves. Unless you're just saying verified handling of mutable state with cycles is extremely difficult in any language with Rust just one example. That would be true. The article also proves Rust ecosystem comes with nice guides on doing that stuff with minimal effort vs what it takes to learn same stuff for C code.




> 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: