undefined

points

[-]

Aw I feel quite sorry for using the word "demonstrable" while not intending to demonstrate anything, in order to avoid any contributions to the project. I apologize for that.

That being said I've found a case that doesn't do much harm even if it's fixed, and is technically not my contribution. You may take a look at that:

https://github.com/oven-sh/bun/pull/30794

by LtWorf16 hours ago|

prev|

[-]

An "unsafe" in rust is like an axiom in mathematics. You can use to prove higher level theorems but it has to make sense.

The second that you start to introduce nonsensical axioms (or bugs in unsafe sections) all your proven correct theorems will be worthless.

by whytevuhuni15 hours ago|

parent|

[-]

But code is not mathematics, so incorrect code is not worthless, it’s just worth less.

It’ll most likely still do 99% of the things people need it to do, there’ll be a an issue created for that broken 1%, and eventually it’ll be iterated upon and fixed.

Unless you’re working on a security boundary of course, there you should treat it like maths.

by LtWorf15 hours ago|

parent|

[-]

Rust doesn't check for logical errors, it checks for memory errors. So every single issue in an unsafe section is a potential CVE.

by whytevuhuni15 hours ago|

parent|

[-]

Of course, but even the presence of CVEs does not make software worthless, it just makes it worth less.

by LtWorf14 hours ago|

parent|

[-]

You don't seem to understand what I'm talking about.

bad axiom -> worthless theorem.

bad unsafe section -> verified safe section is actually not safe.

by whytevuhuni14 hours ago|

parent|

[-]

I’ve understood the distinction. I just don’t like you equating “actually not safe” with “worthless”.

by LtWorf7 hours ago|

parent|

[-]

So you haven't understood the distinction or you're letting your feelings for software get the best of you.

The proof that there are no (for rust's definition of "no") memory bugs becomes worthless, not the entire software itself.

by whytevuhuni6 hours ago|

parent|

[-]

> So you haven't understood the distinction or you're letting your feelings for software get the best of you.

Maybe? I'm not sure.

> The proof that there are no (for rust's definition of "no") memory bugs becomes worthless

I still don't think so, the proof that there are no memory bugs is definitely not worthless, since while the whole proof itself is binary (it is either fully correct or not), its effects act more like coverage, and the more of it that happens to be partially correct, the better.

I think cve-rs is the perfect example of this. Its very existence proves that the borrow checker is already unsound, and with that, the very foundations of Rust's safety guarantees are currently flawed.

TypeScript is another good example, its type system has been repeatedly proven to be unsound, so it's also flawed.

But so what if it's flawed? Many smaller properties of these proofs still happen to hold, and they might prevent 90%+ of CVEs even as flawed as they are.