if the rust compiler is a beast, then i'm going to tame it!
..or get tamed by it depending on how you look at it
Rust has demonstrated that you using a type system as a vehicle for separation logic works, even in imperative languages, and it's nothing as arcane as those immutable functional predecessors would suggest. It did this by making sure the language defines a type system that helps you, by making sure core properties of soundness can be expressed in it.
- soundness requirement for memory access: lifetimes
- soundness requirements for references with value semantics: >
&
/&mut _
- soundness requirements for resources:
Copy
andDrop
- making sure your logic is monotic: traits instead of inheritance, lack of specialization (yes, that's a feature).
- (notably missing: no dependent types; apparently not 'necessary' but I'm sure it could be useful; however, research is heavily ongoing; caution is good)
This allows the standard library to encode all of its relevant requirements as types. And doing this everywhere is its soundness property: safe functions have no requirements beyond the sum of its parameter type,
unsafe functions
can. Nothing new or special there, nothing that makes Rust's notion of soundness special.Basing your mathematical reasoning on separation logic makes soundness reviews local instead of requiring whole program analysis. This is what makes it practical. It did this pretty successfully and principled, but did no single truly revolutionary thing. It's a sum of good bits from the last decade of type system research. That's probably why people refer to it as 'the soundness definition', it's just a very poignant way to say: "we learned that a practical type systems works as a proof checker".
-- HeroicKatora @ https://www.reddit.com/r/cpp/comments/10d4qny/a_call_to_action_think_seriously_about_safety/j4ks225/
This guy hits the nail on the head. I think if C++ can be statically limited to a safe subset, it can still be the better option, especially migrating an existing code base to said subset. However, there is not enough effort going into that because the community doesn't care.
Rust’s numbers speak for themselves. As the number 1 most loved language in the famous stack overflow survey for seven years in a row, it has also recently been released as part of Linux kernel - a feat no language other than C has been able to accomplish. What’s exciting about the language, to me, is that it provides something truly new in the art of how software is built.
Compilers are an error reporting tool with a code generation side-gig.
-- estebank on a Hacker News thread about Rust syntax
It's been 7.5 years since #27060 was reported, but the problem is finally fixed for good. :)
~ Ralf Jung in https://github.com/rust-lang/rust/issues/82523#issuecomment-1416850743
"All the pro C/C++ arguments seem to come down to “Good drivers don’t need seat belts because they don’t get in accidents"
~ otwkme in https://www.reddit.com/r/rust/comments/10rnymj/comment/j6x90x5/?utm_source=share&utm_medium=web2x&context=3
“It’s enjoyable to write Rust, which is maybe kind of weird to say, but it’s just the language is fantastic. It’s fun. You feel like a magician, and that never happens in other languages.”
Parker Timmerman, software engineer
Citation extracted from How Rust went from a side project to the world’s most-loved programming language
I'm not sure if this is fitting for the quote of the week, but I liked the simile enough that I thought it'd be best to let everyone else decide that.
Instead of being dangerous and fun like cigarettes (or French philosophy), C needs to be dangerous and unfun like sewage systems: something that experts handle humble, carefully, and out of necessity, with designs that reflect the societal repercussions of any mistakes.
You've probably come across unsafe. So "unsafe" is a keyword that sort of unlocks super powers and segfaults.
-- Arthur Cohen, in his talk A deep dive inside the Rust frontend for GCC at FOSDEM'23
Edit: There are quite a few quotable lines in this talk.
From this thread:
and as much as i dislike the
cargo-geiger
concept, the name … kind of works
unsafe
is a lot like uranium. it’s just one more metal ore you can process, refine, and machine. it doesn’t combust in atmosphere, it doesn’t corrode or make weird acids. unless you go out of your way to make it dangerous you don’t even have to worry about critical masses. you can work with it pretty normally most of the timebut if you don’t know exactly what it is, what it does, and how to work with it, it will cause mysterious illnesses that only crop up long after you’ve stopped touching it
-- myrrlyn @ https://www.reddit.com/r/rust/comments/11eyu50/i_love_rust_i_have_a_pet_peeve_with_the_community/jahdf3b/
Another thing that I found interesting was hiring Rust developers. Turned out that I thought it would be hard and in a sense I was right. But the last three developers which were hired they didn't use Rust before at all, but still in their second day [..] their commits were already used in production. Pair programming of course helps a lot with this, but I reasonably cannot see anymore that Rust is hard to learn. People can pick it up really really quickly.
-- Markus Klein, "Rust at Aleph Alpha" talk at Rust Linz Meetup (link to youtube)
Memory management is the least interesting application of borrow checking.
The Rust compiler is a thousand unit tests that you don't have to write
-- I built a startup in Rust, I would do it again. | Cloak
(Echoing exactly the reason I'm migrating as much of my development effort as is feasible to Rust.)
Also, give the section it comes from a read. It's possible I misjudged where the boundary lies for the best quote and someone else may want to propose a different cropping.
The generated program is a random sequence of bytes that just happens to take the shape of a seemingly working program by accident. Such is the joy of code that causes UB. You cannot deduce anything from what happens when you execute a program with UB, since that act is by itself meaningless. You need to establish that your program has no UB before making any inference based on what you see the program do after it came out of the compiler.
Ralf Jung on Is read_volatile on uninitialized memory really undefined behavior?
It's a shame the one I proposed came in at the beginning of the week while this one came in at the end and didn't have time to accumulate votes. I think this one deserved it more.
You're not fighting the compiler you're fixing bugs.