Hacker News new | ask | show | jobs
by wolvesechoes 272 days ago
There are valid and safe programs rejected by Rust compiler if you don't go through rituals required to please it (slaping Rc, Refcells etc). No amount of "oh your Rust code is actually something you would ended up with if you would choose C" will change that.
2 comments
simonask 272 days ago
You know, the `unsafe` keyword exists. You’re allowed to use it. If your algorithm is truly safe, and as you say, there are many safe things the borrow checker cannot verify, that’s exactly what `unsafe` is for.

Ideally you can also design a safe API around it using the appropriate language primitives to model the abstraction, but there’s no requirement.

link
crote 272 days ago
Of course. After all, it is mathematically impossible to prove the correctness of all valid and safe programs - the halting problem clearly shows that. The real question should not be "Are there valid and safe programs Rust will reject?" but "How common is it that your well-written valid and safe program will be rejected by the Rust compiler?".

In practice the vast majority will be accepted, and what remains is stuff the Rust compiler cannot prove to be correct. If Rust doesn't like your code, there are two solutions. The first is to go through the rituals to rewrite it as provably-safe code - which can indeed feel a bit tedious if your code was designed using principles which don't map well to Rust. The second is to use `unsafe` blocks - but that means proving its safety is up to the programmer. But as we've historically seen with C and unsafe-heavy Rust code bases, programmers are horrible at proving safety, so your mileage may vary.

I don't want to be the "you're holding it wrong" person, but "Rust rejected my valid and safe program" more often than not means "there's a subtle bug in my program I am not aware of yet". The Rust borrow checker has matured a lot since its initial release, and it doesn't have any trouble handling the low-hanging fruit anymore. What's left is mainly complex and hard-to-reason-about stuff, and that's exactly the kind of code humans struggle with as well.

link