[johnisgood]

Erm what? The article contradicts this. I'd push back on "without jumping through hoops". The article itself demonstrates 6 layers of abstraction (Vec<T> -> RawVec<T> -> RawVecInner -> Unique<u8> -> NonNull<u8> -> *const u8) built on unsafe primitives. The standard library does the hoop-jumping for you, which is valuable, but the hoops exist, they're just relocated.

I bet Vec's implementation is full of unsafe blocks and careful invariant management. Users face different hoops: lifetime wrangling, fighting the borrow checker on valid patterns, Pin semantics, etc. Rust trades runtime overhead for upfront costs: compile-time complexity and developer time wrestling with the borrow checker which is often the right trade, but it's not hoop-free.

The "close to hardware" claim needs qualification too. You're close to hardware through abstractions that hide significant complexity. Ada/SPARK gives formal correctness guarantees but requires proof effort and runtime checks (unless you use SPARK which is a subset of Ada). C gives you actual hardware access but manual memory management. Each has trade-offs - Rust's aren't magically absent.

[zozbot234]

It's fine https://github.com/model-checking/verify-rust-std/issues/283 https://github.com/model-checking/verify-rust-std/pull/481 (But until two weeks ago, it wasn't - you could in theory cause UB by writing purely safe code within the Vec<T> implementation.)

[johnisgood]

I had no idea, that is wild, especially considering how everyone has been outcrying "Rust is safe". Thanks for the info though.

One should wonder what else is there... but they do not wonder, they are sadly rigid with their thinking that Rust is the perfect memory safe language with zero runtime overhead.

[zozbot234]

It's not real unsoundness because it only applies within the private implementation details of Vec<T> - you still can't cause UB from outside code. But it's a real oversight that only proves how hard writing unsafe code is.

[Klonoar]

You know you can discuss languages without the weird emotional labeling from your last paragraph, right?

Plenty of people wonder. It’s part of building the language.

[johnisgood]

Fair enough.

[ozy]

Most of those are abstractions, but not a runtime overhead. NonNull even enables an optimization not available to most other languages.

And you can wonder, is this accidental complexity? Or is this necessary complexity?