"borrow checker invariants" section of the "leveraging the type system" chapter #2867

tall-vase · 2025-09-01T16:19:59Z

Adds materials on the "leveraging the type system/borrow checker invariants" subject.

I'm still calibrating what's expected subject-and-style wise, so do spell out things where I've drifted off mark.

…n to lifetime connections

google-cla · 2025-09-01T16:20:03Z

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

LukeMathWalker · 2025-09-02T23:47:27Z

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants.md

+
+- The borrow checker has been used to prevent use-after-free and multiple mutable references up until this point.
+
+- This example uses the ownership & borrowing rules to model the opening and closing of a door. We can try to open a door with a key, but if it's the wrong key the door is still closed (here represented as an error.)


That is indeed the case in the example, but it's not related to ownership/borrowing, isn't it?
If I'm interpreting things correctly, the example connects to the topic by intentionally consuming a door by value whenever it changes state, thus making it impossible for a door to be both open and closed at the same time.
We should point the instructor in that direction, if that's what we mean by it.

I think "consuming .. by value" is an example of "ownership", but making this more explicit is good.

Yes, "consuming a value" is still within the bounds of what the borrow checker cares about here (I'll make this more clear)

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/generalizing-ownership.md

LukeMathWalker · 2025-09-02T23:49:32Z

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/generalizing-ownership.md

+pub struct InternalData;
+pub struct Value(InternalData);
+
+fn shared_use(value: &Value) -> &InternalData {
+    &value.0
+}
+
+fn exclusive_use(value: &mut Value) -> &mut InternalData {
+    &mut value.0
+}
+
+fn deny_future_use(value: Value) {}
+
+let mut value = Value(InternalData);
+let deny_mut = shared_use(&value);
+let try_to_deny_immutable = exclusive_use(&mut value); // ❌🔨
+let more_mut_denial = &deny_mut;
+deny_future_use(value);
+let even_more_mut_denial = shared_use(&value); // ❌🔨


In the speaker notes, we should elaborate as to what the example is trying to show and how it relates to the concepts we're discussing.
This is a bit too implicit for me on this slide.

LukeMathWalker · 2025-09-02T23:52:44Z

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/single-use-values.md

+```rust,editable
+fn main() {
+pub struct Key;
+
+// Pretend this is a cryptographically unique, use-once number.
+pub struct Nonce(u32);
+
+// It's unsafe to declare a nonce directly! In practice,
+// this would be done with an RNG source, and potentially
+// a timestamp.
+unsafe fn new_nonce_from_raw(nonce: u32) -> Nonce {
+    Nonce(nonce)
+}
+
+let nonce = unsafe { new_nonce_from_raw(1337) };
+let data_1: [u8; 4] = [1, 2, 3, 4];
+let data_2: [u8; 4] = [4, 3, 2, 1];
+let key = Key;
+
+// The key and data can be re-used, copied, etc. but the nonce cannot.
+fn encrypt(nonce: Nonce, key: &Key, data: &[u8]) {}
+
+encrypt(nonce, &key, &data_1);
+encrypt(nonce, &key, &data_2); // 🛠️❌
+}
+```


I think the new_non_from_raw/unsafe aspect add unnecessary noise to the example. We don't need to go into the details as to how a Nonce is constructed, we just need a constructor/generator to exist.

In practice there's probably no way to construct a fixed nonce (whether unsafe or not). So that part is a bit misleading. It's also a bit confusing that let nonce = Nonce(1234) would also work here, due to being in the same module. Maybe put Nonce in a submodule and do something succinct but effective to make a new() method that generates a unique Nonce on every call (e.g., using system rand is probably fine here).

LukeMathWalker · 2025-09-02T23:53:35Z

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/aliasing-xor-mutability.md

+
+<details>
+
+- This example shows how we can use the "Aliasing XOR Mutability" rule when it comes to shared and mutable references to model safe access to transactions for a database. This is a loose sketch of such a model, and rust database frameworks you use may not look anything like this in practice.


It might be useful to recall in layman's terms what "Aliasing XOR Mutability" implies, since a lot of folks may not be familiar with that precise terminology.

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/aliasing-xor-mutability.md

LukeMathWalker · 2025-09-03T00:01:13Z

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/aliasing-xor-mutability.md

+<!-- Entirely reasonable to reframe the example off this contradiction, but I think it has pedagogical value regardless. -->
+- Tangential: We could instead have the `get_transaction` method return a mutable reference off a mutable reference to self (`fn get_transaction(&mut self) -> &mut TransactionInterface`) but we're trying to show off the ways shareable and mutable references exclude each other here.


Re-reading the example, it does feel somewhat too artificial for showing off this specific concept (e.g. compared to using a Transaction and commit as a way to showcase that you can "consume" to end the lifecycle of a resource).

djmitche · 2025-09-06T22:03:53Z

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants.md

+
+- The borrow checker has been used to prevent use-after-free and multiple mutable references up until this point.
+
+- This example uses the ownership & borrowing rules to model the opening and closing of a door. We can try to open a door with a key, but if it's the wrong key the door is still closed (here represented as an error.)


I think "consuming .. by value" is an example of "ownership", but making this more explicit is good.

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants.md

djmitche · 2025-09-06T22:06:21Z

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/generalizing-ownership.md

+
+<details>
+
+- To use the borrow checker as a problem solving tool, we will need to "forget" that the original purpose of it is to prevent mutable aliasing in the context of concurrency, instead imagining and working within situations where the rules are the same but the meaning is slightly different.


This seems redundant to the first slide in the segment

djmitche · 2025-09-06T22:07:30Z

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/generalizing-ownership.md

+
+- In rust's borrow checker we have access to three different ways of "taking" a value:
+
+<!-- TODO: actually link to the RAII section when it has been merged. -->


This is a callback to several sections in the fundamentals course. I suspect you could summarize this in one sentence, just using the syntax and names of each way of taking values, and assume the instructor / student understands or can look those up.

The important part here is the context – the rules are being laid out in with the knowledge that we're going to be using them to restrict the shape of APIs rather than specifically to avoid memory issues. You're right that it could be more clear that this is the context these rules are being reiterated in :)

djmitche · 2025-09-06T22:08:15Z

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/generalizing-ownership.md

+
+- Important to note that every `&T` and `&mut T` has an _implicit lifetime._ We get to avoid annotating a lot of lifetimes because the rust compiler can infer the majority of them. See: [Lifetime Elision]("../../../../../lifetimes/lifetime-elision.md")
+
+- Potentially relevant: show how we can replace a lot of the `&` and `&mut` here with `&'a` and `&'a mut`.


Are lifetimes relevant for this sort of generalization of ownership? I think this is best left until the slide later in the section.

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/aliasing-xor-mutability.md

djmitche · 2025-09-06T22:30:57Z

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/lifetime-connections.md

+
+<details>
+
+- PhantomData lets developers "tag" types with type and lifetime parameters that are not "really" present in the struct or enum.


I think this is covered in the typestate section? Maybe just reference that, and focus on the new usage here of PhantomData encoding a lifetime.

I couldn't find reference to PhantomData in the typestate section, though I could have missed something.

I'm sorry -- I was thinking of typestate patterns in general which often uses marker types with PhantomData. But you're correct, the serializer example in #2821 does not use PhantomData, as the state contains data. So, this sentence is fine :)

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/lifetime-connections.md

djmitche · 2025-09-06T22:36:35Z

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/lifetime-connections.md

+
+- [`BorrowedFd`](https://rust-lang.github.io/rfcs/3128-io-safety.html#ownedfd-and-borrowedfdfd) uses these captured lifetimes to enforce the invariant that "if this file descriptor exists, the OS file descriptor is still open" because a `BorrowedFd`'s lifetime parameter demands that there exists another value in your program that has the same lifetime as it, and this has been encoded by the API designer to mean _that value is what keeps the access to the file open_. Its counterpart `OwnedFd` is instead a file descriptor that closes that file on drop.
+
+- Lifetimes need to come from somewhere! We can't build functions of the form `fn lifetime_shenanigans<'a>(owned: OwnedData) -> &'b Data` (without tying `'b` to `'a` in some way). Lifetime elision hides where a lot of lifetimes come from, but that doesn't mean the explicitly named lifetimes "come from nowhere."


It might be helpful to suggest writing out the elisions in get_erased. In fact, I think the latest stable has a new lint for this use of '_ to reference the elided lifetime in the argument, so perhaps spelling this method's lifetimes out in the example is best.

tall-vase added 5 commits August 27, 2025 16:07

Initial draft of the 'borrow checker invariants' section

b771e7f

Elaborate more on the cryptography example

3831858

Begin expanding the slide notes, rename the external resources sectio…

a81b55a

…n to lifetime connections

Get this section into a 'review ready' state.

0b4318f

Reset all minutes on the borrowck invariants section to 0

728af30

tall-vase added the deep_dives/idiomatic label Sep 1, 2025

tall-vase changed the title ~~"borrow checker invariants" section of the~~ "borrow checker invariants" section of the "leveraging the type system" chapter Sep 1, 2025

LukeMathWalker reviewed Sep 2, 2025

View reviewed changes

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/generalizing-ownership.md Show resolved Hide resolved

LukeMathWalker reviewed Sep 2, 2025

View reviewed changes

src/idiomatic/leveraging-the-type-system/borrow-checker-invariants/aliasing-xor-mutability.md Outdated Show resolved Hide resolved

LukeMathWalker reviewed Sep 3, 2025

View reviewed changes

djmitche reviewed Sep 6, 2025

View reviewed changes

tall-vase added 2 commits September 8, 2025 16:30

General editing pass based off feedback

a37a272

Minor editing

88852f2


		- The borrow checker has been used to prevent use-after-free and multiple mutable references up until this point.

		- This example uses the ownership & borrowing rules to model the opening and closing of a door. We can try to open a door with a key, but if it's the wrong key the door is still closed (here represented as an error.)


		<details>

		- This example shows how we can use the "Aliasing XOR Mutability" rule when it comes to shared and mutable references to model safe access to transactions for a database. This is a loose sketch of such a model, and rust database frameworks you use may not look anything like this in practice.

		<!-- Entirely reasonable to reframe the example off this contradiction, but I think it has pedagogical value regardless. -->
		- Tangential: We could instead have the `get_transaction` method return a mutable reference off a mutable reference to self (`fn get_transaction(&mut self) -> &mut TransactionInterface`) but we're trying to show off the ways shareable and mutable references exclude each other here.


		<details>

		- To use the borrow checker as a problem solving tool, we will need to "forget" that the original purpose of it is to prevent mutable aliasing in the context of concurrency, instead imagining and working within situations where the rules are the same but the meaning is slightly different.


		- In rust's borrow checker we have access to three different ways of "taking" a value:

		<!-- TODO: actually link to the RAII section when it has been merged. -->


		- Important to note that every `&T` and `&mut T` has an _implicit lifetime._ We get to avoid annotating a lot of lifetimes because the rust compiler can infer the majority of them. See: [Lifetime Elision]("../../../../../lifetimes/lifetime-elision.md")

		- Potentially relevant: show how we can replace a lot of the `&` and `&mut` here with `&'a` and `&'a mut`.


		<details>

		- PhantomData lets developers "tag" types with type and lifetime parameters that are not "really" present in the struct or enum.


		- [`BorrowedFd`](https://rust-lang.github.io/rfcs/3128-io-safety.html#ownedfd-and-borrowedfdfd) uses these captured lifetimes to enforce the invariant that "if this file descriptor exists, the OS file descriptor is still open" because a `BorrowedFd`'s lifetime parameter demands that there exists another value in your program that has the same lifetime as it, and this has been encoded by the API designer to mean _that value is what keeps the access to the file open_. Its counterpart `OwnedFd` is instead a file descriptor that closes that file on drop.

		- Lifetimes need to come from somewhere! We can't build functions of the form `fn lifetime_shenanigans<'a>(owned: OwnedData) -> &'b Data` (without tying `'b` to `'a` in some way). Lifetime elision hides where a lot of lifetimes come from, but that doesn't mean the explicitly named lifetimes "come from nowhere."

"borrow checker invariants" section of the "leveraging the type system" chapter #2867

Are you sure you want to change the base?

"borrow checker invariants" section of the "leveraging the type system" chapter #2867

Uh oh!

Conversation

tall-vase commented Sep 1, 2025

Uh oh!

google-cla bot commented Sep 1, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

LukeMathWalker Sep 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

LukeMathWalker Sep 2, 2025 •

edited

Loading