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:
The second that you start to introduce nonsensical axioms (or bugs in unsafe sections) all your proven correct theorems will be worthless.
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.
bad axiom -> worthless theorem.
bad unsafe section -> verified safe section is actually not safe.
The proof that there are no (for rust's definition of "no") memory bugs becomes worthless, not the entire software itself.
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.
I'm not sure I'm following what you're saying here. In the rewrite blog post it has been stated that the Rust port landed in a place where it passes 100% of the existing test suite and does so without some of the known memory leaks of the Zig version that they were aware of and didn't know how to address.
Sure, there's no guarantee that the port didn't introduce new bugs and most likely it did, but the 1.4 version has not been released yet, so I don't think a direct comparison of a long-time "stable" version and the just-landed full rewrite is meaningfully helpful.
> "Potential memory issue" can originate in unsafe blocks and safe code that are able to alternate the input condition of these unsafe blocks. Guess what? That still counts towards 100% in this code base, hence the abomination remark.
But that just means that once you get rid of the unsafe block, you're pretty much guaranteed by the Rust compiler to be memory-safe. This means that all your potential memory landmines are annotated in the code and once you disarm them all, you're memory-safe.
I don't understand how what you're saying contradicts any of my statements.
> Not as easy as it sounds. They are like threads in a yarn ball, if there are one or two ends visible it's easier to sort them out.
Still easier than the Zig version, where all the same things you've mentioned apply, but also there's no visible indication of progress and issues are unmarked and could be pretty much anywhere.
> It's too early to declare it as anything remotely close to a win, optimistically saying.
Based on the rewrite blog post it's pretty clear that the Rust version is outperforming the Zig version by pretty much every measurable metric at this point.
I think the backlash is mostly focused on the ideological opposition to fully AI-authored 1MLOC+ PR approach they took.
They can't mention what they don't know. And that's the exact reason I'm against this: doing a port without being able to tell what is correct is asking for a disaster, obviously.
I've checked their posts and blogs for a few times, and I'm quite sure they don't know any of these to write about them.
> the 1.4 version has not been released yet
Let's hope the repeated delays (it was scheduled for last week) are not for quality issues, otherwise I'll only be half correct. It appears that all the MIRI errors are not stopping them though. (They have a script to run it but most probably it just fails and they don't care. Personally I'm not executing any of bun's code to avoid summoning nasal demons, so I actually don't know for sure)
> get rid of the unsafe block
Would be possible if they are not disregarding everything else going for numbers. E.g. they are actively increasing the unsafe surface by rewriting some code in SIMD C++ (https://github.com/oven-sh/bun/pull/33032). As if no Rust solutions already exist.
> Still easier than the Zig version
Well, this is true but only realizable if they know how to deal with the new problems emerging during the process. My current conclusion is that they don't.
> ideological
For me it's methodological as explained above.