←back to thread

169 points signa11 | 1 comments | | HN request time: 0s | source
Show context
smodo ◴[] No.41875908[source]
I’m not very well versed in kernel development. But I am a Rust dev and have observed the discussion about Rust in Linux with interest… Having said that, this part of the article has me baffled:

>> implementing these features for a smart-pointer type with a malicious or broken Deref (the trait that lets a programmer dereference a value) implementation could break the guarantees Rust relies on to determine when objects can be moved in memory. (…) [In] keeping with Rust's commitment to ensuring safe code cannot cause memory-safety problems, the RFC also requires programmers to use unsafe (specifically, implementing an unsafe marker trait) as a promise that they've read the relevant documentation and are not going to break Pin.

To the uninformed this seems like crossing the very boundary that you wanted Rust to uphold? Yes it’s only an impl Trait but still… I can hear the C devs now. ‘We pinky promise to clean up after our mallocs too!’

replies(7): >>41875965 #>>41876037 #>>41876088 #>>41876177 #>>41876213 #>>41876426 #>>41877004 #
foundry27 ◴[] No.41875965[source]
Rust’s whole premise of guaranteed memory safety through compiletime checks has always been undermined when confronted with the reality that certain foundational operations must still be implemented using unsafe. Inevitably folks concede that lower level libraries will have these unsafe blocks and still expect higher level code to trust them, and at that point we’ve essentially recreated the core paradigm of C: trust in the programmer’s diligence. Yeah Rust makes this trust visible, but it doesn’t actually eliminate it in “hard” code.

The punchline here, so to speak, is that for all Rust’s claims to revolutionize safety, it simply(!) formalizes the same unwritten social contract C developers have been meandering along with for decades. The uniqueness boils down to “we still trust the devs, but at least now we’ve made them swear on it in writing”.

replies(10): >>41876016 #>>41876042 #>>41876122 #>>41876128 #>>41876303 #>>41876330 #>>41876352 #>>41876459 #>>41876891 #>>41877732 #
wbl ◴[] No.41876016[source]
The difference is every line of C can do something wrong while very few lines of Rust can. It's much easier to scrutinize a small well contained class with tools like formal methods than a sprawling codebase.
replies(2): >>41876538 #>>41877544 #
uecker ◴[] No.41876538[source]
If you limited wrong to "memory safe" and also ignore that unsafe parts violating invariants can make safe parts of Rust to be wrong.
replies(1): >>41876669 #
Dylan16807 ◴[] No.41876669{3}[source]
> If you limited wrong to "memory safe"

Yes, because this is a discussion about the value of "unsafe", so we're only talking about the wrongs that are enabled by "unsafe".

> and also ignore that unsafe parts violating invariants can make safe parts of Rust to be wrong.

If I run a line of code that corrupts memory, and the program crashes 400 lines later, I don't say the spot where it crashes is wrong, I say the memory corrupting line is wrong. So I disagree with you here.

replies(1): >>41877536 #
uecker ◴[] No.41877536{4}[source]
It does not invalidate an argument that you do not want to talk about it.

Regarding the second point: yes, you can then blame the "unsafe" part but the issue is that the problem might not be so localized as the notion of "only auditing unsafe blocks is sufficient" implies. You may need to understand the subtle interaction of unsafe blocks with the rest of the program.

replies(3): >>41877958 #>>41878776 #>>41882921 #
1. Dylan16807 ◴[] No.41882921{5}[source]
Unsafe blocks have to uphold their invariants while accepting any possible input that safe code can give them. Any subtle interactions enabled by "unsafe" need to be part of the invariants. If they don't do that, it's a bug in the unsafe code, not the safe code using it.

If done properly, you can and should write out all the invariants, and a third party could create a proof that your code upholds them and they prevent memory errors. That involves checking interactions between connected unsafe blocks as a combined proof, but it won't extend to "the rest of the program" outside unsafe blocks.