4 ms·

Eh. You can write, and people have written, formal proofs about C code too. In fact, the difference between Rust and C in terms of safety isn't very large if yo

Eh. You can write, and people have written, formal proofs about C code too. In fact, the difference between Rust and C in terms of safety isn't very large if you have an infinite budget to put toward proving all the code that you write correct. The safety benefits of Rust appear when you aren't willing to formally prove all the code you write correct. That's because you only have to prove the unsafe code, plus the memory model, correct in order to guarantee memory safety for the entire program. This is less burdensome than in C, where to do the same you have to prove correctness properties about the specific code that makes up the whole program. Rust makes it easier to prove certain properties about the program (far easier in the case of memory safety), but it was always possible.

zozbot234 5y ago
> Eh. You can write, and people have written, formal proofs about C code too. Not without a formal model of C, and the C standard is only an informal, natural-language text. Rust having memory safety as its express goal (which is basically table stakes for any sort of workable language semantics) means that it's at least realistic to think about a formal semantics for Safe Rust. Then you "just" need to deal with the uncomfortable reality that lots of Safe Rust facilities actually bottom out into Unsafe Rust, which is why it turns out you must care about its semantics too. But the hope is ultimately that the small portion of real-world Rust codebases that's Unsafe Rust might not "infect" the Safe Rust to the point of making verification as practically unworkable as in C.
- nullc 5y ago
  There are formalization of C, e.g. compcert, which also compiles to machine code in a way that should guarantee proofs all the way though execution (assuming the machine modeling is correct). It seems like it is a long way off from being possible to do that for rust.
xavxav 5y ago
I’m doing my PhD on the formal verification of Rust, and while you’re right that safe code provides a lot of informal advantages it also dramatically simplified form reasoning. In particular, the dirty secret of C verifiers is that they don’t handle pointers all that well. Either you find yourself doing a lot of manual proof work or you have to dramatically simplify the memory model. In contrast, when verifying safe Rust, the rules of the borrow checker allow us to dramatically simplify the verification work. All of a sudden verifying a manual memory program with pointers (borrows) becomes as simple as verifying a basic imperative language. I’ve been working on a tool: https://github.com/xldenis/creusot https://github.com/xldenis/creusot to put this into practice On the other hand, the moment you dive into unsafe, all bets are off and you find yourself wading through the marshes of (weak) memory models with your favorite CSL as your only friend.
- zozbot234 5y ago
  > I’ve been working on a tool: https://github.com/xldenis/creusot https://github.com/xldenis/creusot to put this into practice Note that there are other tools trying to deal with formal statements about Rust programs. AIUI, Rust developers are working on forming a proper team or working group for pursuing these issues. We might get a RFC-standardized way of expressing formal/logical conditions about Rust code, which would be a meaningful first step towards supporting proof-carrying code directly within Rust.

zozbot234 5y ago

> Eh. You can write, and people have written, formal proofs about C code too. Not without a formal model of C, and the C standard is only an informal, natural-language text. Rust having memory safety as its express goal (which is basically table stakes for any sort of workable language semantics) means that it's at least realistic to think about a formal semantics for Safe Rust. Then you "just" need to deal with the uncomfortable reality that lots of Safe Rust facilities actually bottom out into Unsafe Rust, which is why it turns out you must care about its semantics too. But the hope is ultimately that the small portion of real-world Rust codebases that's Unsafe Rust might not "infect" the Safe Rust to the point of making verification as practically unworkable as in C.

nullc 5y ago
There are formalization of C, e.g. compcert, which also compiles to machine code in a way that should guarantee proofs all the way though execution (assuming the machine modeling is correct). It seems like it is a long way off from being possible to do that for rust.

xavxav 5y ago

I’m doing my PhD on the formal verification of Rust, and while you’re right that safe code provides a lot of informal advantages it also dramatically simplified form reasoning. In particular, the dirty secret of C verifiers is that they don’t handle pointers all that well. Either you find yourself doing a lot of manual proof work or you have to dramatically simplify the memory model. In contrast, when verifying safe Rust, the rules of the borrow checker allow us to dramatically simplify the verification work. All of a sudden verifying a manual memory program with pointers (borrows) becomes as simple as verifying a basic imperative language. I’ve been working on a tool: https://github.com/xldenis/creusot https://github.com/xldenis/creusot to put this into practice On the other hand, the moment you dive into unsafe, all bets are off and you find yourself wading through the marshes of (weak) memory models with your favorite CSL as your only friend.

zozbot234 5y ago
> I’ve been working on a tool: https://github.com/xldenis/creusot https://github.com/xldenis/creusot to put this into practice Note that there are other tools trying to deal with formal statements about Rust programs. AIUI, Rust developers are working on forming a proper team or working group for pursuing these issues. We might get a RFC-standardized way of expressing formal/logical conditions about Rust code, which would be a meaningful first step towards supporting proof-carrying code directly within Rust.