TWiR quote of the week

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

@kyo@haunted.computer on Mastodon

3 Likes

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 and Drop
  • 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/

8 Likes

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.

2 Likes

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.

3 Likes

Another self-suggestion:

Robust Underpinnings, Strong Technique

-- yours truly on twitter

2 Likes

Compilers are an error reporting tool with a code generation side-gig.

-- estebank on a Hacker News thread about Rust syntax

11 Likes

A post was split to a new topic: Mutable vs exclusive reference

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

6 Likes

"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

4 Likes

“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

8 Likes

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.

-- The unsafe language doom principle

5 Likes

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.

6 Likes

From this thread:

4 Likes

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 time

but 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/

14 Likes

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)

9 Likes

Memory management is the least interesting application of borrow checking.

Fixing the next 10 000 aliasing bugs

6 Likes

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.

14 Likes

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?

15 Likes

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.

2 Likes

You're not fighting the compiler you're fixing bugs.

Also from I built a startup in Rust, I would do it again.

12 Likes