Unsafe Rust versus C and C++

Is that not in direct contrast to https://lwn.net/Articles/1007973/ ? At least in the context of the Linux kernel?

>[...]but the definition of "unsafe code" is "stuff the compiler can't prove is correct"[...]

A minor technicality: the compiler is not proving the correctness of the code, it is (meant to be) proving the memory safety/absence of undefined behavior. In the sense that memory safe code without undefined behavior can have logic bugs.

>All safe code MUST be fully defined, and MUST be provably correct (bugs, cockups, and acts of God excepted).

Did you mean unsafe?

But even then, this does not always hold in practice.

github.com/rust-lang/rust/commit/71f5cfb21f3fd2f1740bced061c66ff112fec259

cve.org/CVERecord?id=CVE-2024-27308

>100% of C/C++ programmers are likely to step on an unsafe landmine several times a year.

I do not believe this is true, but I do believe that Rust makes some aspects significantly easier, and not only its borrow checking and solver and lifetimes handling, though in the specific case of Rust that also comes with penalties in the unsafe subset. One great advantage is Rust's pattern matching and disjoint unions, taken from functional programming. And one thing that makes C and C++ error prone for some cases is that C and C++ are ancient languages that have a lot of cruft and baggage. I do prefer functional programming, and hope that C++ will get a good and robust implementation of both pattern matching and disjoint unions (C arguably has a limited scope), but Rust has significant issues. To be perfectly frank, I wonder if a Rust killer in the future may greatly iterate on and improve and be closer to what many of us hoped that Rust would be.

>The definition of "unsafe" code is "stuff the compiler can't prove correct". And you're moaning that the compiler writers aren't mathematical gods because they can't (yet) prove some very tricky problems. And other problems are just plain insolvable.
>
>THAT is why unsafe code is hard. Because the maths behind it is hard. Knuth ranks his problems from 0 is "easy" to (iirc) 5 is "if you can solve it it's worth a PhD". As soon as you start programming "unsafe", you are dealing with code where the proofs are 4 or 5 on the scale - if it's even provable!

But these issues are not purely theoretical, and appears to cause not only users but also language developers trouble.

https://github.com/lcnr/solver-woes/issues/1

>Even worse, there may be changes to asymptotic complexity of some part of the trait system. This can cause crates which start to compile fine due to the stabilization of the new solver to hang after regressing the complexity again. This is already an issue of the current type system. For example rust-lang/rust#75443 caused hangs (rust-lang/rust#75992), was reverted in rust-lang/rust#78410, then landed again after fixing these regressions in rust-lang/rust#100980 which caused yet another hang (rust-lang/rust#103423), causing it to be reverted yet again in rust-lang/rust#103509.

And the Rust language developers made multiple blog posts discussing their work on the new solver, and on trying to make it backwards compatible.

There is a comment where I discuss the language design of Rust and related issues https://lwn.net/Articles/1008103/ . One could argue that requiring a complex solver, that in practice may end up with holes, has practical trade-offs in the language design. I recall that Bjarne Stroustrup was against any language feature that would require complex solvers. I wonder if part of the reasoning is that it would make it harder to implement correct compilers. Which may be consistent with some of the headaches that some apparently really skilled people among the Rust language developers appear to be dealing with. I do not envy their position, their challenge looks difficult.

>And now you are really coming over as lying by omission. Sorry.

I do not agree with this at all, and as far as I can tell, you are completely wrong about this.