This isn't quite accurate; Mojo uses the same memory safety approach as Rust. It has some mutable aliasing, but only intra-function, so in practice programs will be pretty much Rust-shaped.
1,963 karma · joined May 25, 2018
Ante is making some very intriguing steps forward in memory safety design and I thought others would find it interesting too.
As a thought experiment, I've been imagining how this would handle an architecture like e.g. Google Earth's, where a program's classes are divided into multiple "layers". For example, an upper "business logic" layer (DocumentManager, Document, CardManager, Card, StateManager) might have references to the more general "services" lower layer (NetworkService, FileService).
With Nick's system, we could have a group annotation on these various upper-layer classes, like e.g. `Document[s: group IService]`. With these annotations, these upper-layer classes can have references to the services themselves (though not their contents). This might let services' methods mutate the services' contents even though others have references to them (though not their contents). The services' methods would have to communicate that they're modifying the contents of the services (via a `mut` annotation), and the compiler would prevent holding references to the services' contents across those callsites. But also, those contents are private anyway, so the user wouldn't have those references anyway.
If that turns out to be true (Nick and I are still exploring it) then he's found a way to make borrowing work for some DAG-shaped program architectures, rather than just strictly tree-shaped architectures.
On top of that, if we compose this approach with linear types, I think we can get at least halfway towards compile-time-memory-safe back-references. TBD whether that works, but that would be pretty exciting.
TL;DR: My saying it only supports tree-shaped programs is me hedging and being conservative.
Still, until these things are proven to work, I should be more consistent in when I'm conservative vs optimistic. I'll update the article to address that. Thanks for pointing that out and helping me be more consistent!
This new approach still requires us to be mindful of our data layout. Not caring about data layout is still definitely a strength of GC and RC. I'm actually hoping to find a way to blend Nick's approach seamlessly with reference counting (preferably without risking panics or deadlocks) to get the best of both worlds, so that we can consider it for Mojo. I consider that the holy grail of memory safety, and some recent developments give me some hope for that!
(Also, I probably shouldn't mention it since it's not ready, but Nick's newest model might have found a way to solve that for separate-chaining hash maps where addresses are stable. We might be able to express that to the type system, which would be pretty cool.)
TL;DR: Mutability is tracked at the group level, so we can share an immutable group with any number of threads (especially good with structured concurrency) or lend a mutable group to a single other thread. References themselves are still aliasable, regardless of the group's mutability.
Taking an existing (mutable, aliasing) group and temporarily interpreting it as immutable has precedent (I did it in Vale [0]) so I like the approach, but I might be biased ;)
(This is from my memory of how Nick's proposal works, I'll ask him to give a better answer once morning hits his Australia timezone)
[0] https://verdagon.dev/blog/zero-cost-borrowing-regions-part-1...
It was interesting enough that I knew I had to write a post about it. Happy to answer any questions!
I think the need for Pin could then disappear, because the user would have no way to destroy it, since it's opaque and elsewhere on the heap, and therefore no way to move it (because having move-constructors implies that moving is conceptually destroying then recreating things).
OP shows the benefits of a linear RC that tracks references dynamically, and one can even imagine a version where the compiler tracks the references instead.
For example (for those who are more familiar with Rust) imagine that it had linear types and that we used them for matthieum's static-RC [0] (like suggested by frank-king at [1] to prevent leaks) and you'd have a pretty good idea of linear static RC.
I also talked about a possible alternative linear static RC at [2] and [3] (I didn't explain it well at all, happy to elaborate), though lately I suspect that one would need to add a GhostToken-ish [4] substance to allow safely reading/writing the shared value, or perhaps a RefCell.
I suspect that something like GhostToken could also solve OP's restriction that types be opaque, if Haskell has something like GhostToken... I could be wrong on that though.
[0] https://github.com/matthieu-m/static-rc
[1] https://github.com/matthieu-m/static-rc/issues/7
[2] "Linear reference counting" in https://verdagon.dev/grimoire/grimoire#the-list
[3] https://www.reddit.com/r/rust/comments/1d06gjo/comment/l61qm...
[4] https://www.reddit.com/r/rust/comments/p5f78s/ghostcell_sepa...
TL;DR: The lowest common denominator between Rust and any other memory-safe language is a borrow-less affine type.
The key insight is that Rust is actually several different mechanisms stacked on top of each other.
To illustrate, imagine a program in a Rust-like language.
Now, refactor it so you don't have any & references, only &mut. It actually works, if you're willing to refactor a bit: you'll be storing a lot of things in collections and referring to them by index, and cloning even more, but nothing too bad.
Now, go even further and refactor the program to not have any &mut either. This requires some acrobatics: you'll be temporarily removing things from those collections and moving things into and out of functions like in [2], but it's still possible.
You're left with something I refer to as "borrowless affine style" in [1] or "move-only programming" in [0].
I believe that's the bare minimum needed to interoperate with Rust in a memory safe way: unreference-able moveable types.
The big question then becomes: if our language has only these moveable types, and we want to call a Rust function that accepts a reference, what then?
I'd say: make the language move the type in as an argument, take a temporary reference just for Rust, and then move-return the type back to the caller. The rest of our language doesn't need to know about borrowing, it's just a private implementation detail of the FFI.
These weird moveable types are, of course, extremely unergonomic, but they serves as a foundation. A language could use these only for Rust interop, or it could go further: it could add other mechanisms on top such as & (hard), or &mut (easy), or both (like Rust), or a lot of cloning (like [3]), or generational references (like Vale), or some sort of RefCell/Rc blend, or linear types + garbage collection (like Haskell) and so on.
(This is actually the topic of the next post, you can tell I've been thinking about it a lot, lol)
[0] "Move-only programming" in https://verdagon.dev/grimoire/grimoire#the-list
[1] "Borrowless affine style" in https://verdagon.dev/blog/vale-memory-safe-cpp
[2] https://verdagon.dev/blog/linear-types-borrowing
[3] https://web.archive.org/web/20230617045201/https://degaz.io/...
PS. Congrats! https://verdagon.dev/blog/easter-egg-notes
(One caveat is for linears in globals, which aren't implemented in Vale yet. We haven't decided which strategy we're going with there, but TFA talks about some)
1. drop_into(list, func): It consumes the list, calling the given `func` for each element.
2. expect_empty(list): Consumes the list, panicking if the list isn't empty.
Alas, I haven't started on sealed interfaces yet. Right now I'm occupied with the Rust interop; I'm hoping we can be able to seamlessly e.g. `import rust.std.collections.Vec<i32>;` and have it work. A lot of pieces have to fall into place for that to work though, especially since that's generic and Rust doesn't even have a stable ABI. It's kicking my ass, and I'm having a lot of fun with it!
This godbolt hopefully illustrates: https://godbolt.org/z/qqMnnKbnd though apologies if it's not too clear.
If C++ didn't have its quirks, you'd fundamentally be correct. Higher RAII can almost completely be implemented by this one sentence: make destruction private. (In fact, that's why Vale's `destruct` keyword is file-private)
1. In RC and tracing GC languages, a linear object would need exactly one special "linear" reference to it, which would be responsible for eventually "consuming" (though not deleting) the object by handing it to its final destination function. (You can tell, I'm trying real hard to not say destructor here)
2. In single-ownership languages like C++, Rust, etc. we've been conflating the destructor to handle two things: fulfilling the object's final purpose, and handling exceptions/panics. It seemed convenient at the time, but it also prevented linear types.
But honestly, I think we were just stuck in a local maximum. There was no reason to change those points because we didn't know about higher RAII, and we didn't know about higher RAII because those two points prevented linear types.
But with more of us exploring this new area (Vale, Austral, maybe even Mojo!), I daresay we'll one day see linear types and higher RAII entering the mainstream. Especially if someone can come up with a better name!
Even if a language really wanted to have linear types in reference-counted objects, I don't think we'd see cycles in practice. Generally, for a reference-counted object to contain a linear type, we'd need exactly one reference to be the special "linear reference" (think a linear flavor of unique_ptr) which has ultimate responsibility for "consuming" (albeit not deleting) the contents. Making a unique_ptr cycle is much harder than making a regular RC cycle, so I'm not too worried, even if it is theoretically possible.
Re: trivial moves, I'm not sure what you mean. The system works through the entire program, not just local variables. Also, the `onException` method would also handle panics. Hope that helps!
This is my favorite part of language design: you get to play with weird ideas and see how the implications cascade through the rest of the program. It kind of blew my mind when a linear type solved a caching problem.
Now it's kind of a curse, because any time I code in a normal language (even the modern ones like Scala and Rust) I see places (concurrency, coroutines, etc) where we could have statically prevented these bugs.
Biggest example I've seen: wanting to use Java for a web server where a 10-line node server did wonderfully. Or similarly, wanting to use async/await in Rust when threads are more than sufficient.
Sometimes I think we make our problems unnecessarily complex by chasing efficiency perfection.
This brings me back. I used to make little games for Palm OS, and I was so excited for the next version of the OS which would let one use the (then new) Palm OS Development Suite to make programs. It was also the last OS I've used where an app had a central event loop. Everything else today has UI frameworks that handle it for you. Things are easier now, but I still miss it.
Perhaps there are other mechanisms out there too.
I feel like the ability to destroy another thread isnt inherently bad, just... bad with today's languages. Just a feeling though.
Rather, I think that the static analysis we see in today's languages just isn't powerful/flexible enough to reason about safety in a lot of the patterns that we know are safe. I'm also uncertain if it can _ever_ catch up to what we know to be safe, but I wouldn't be surprised if we get there in a few hundred years.
For example, borrow checking is a step forward and can guarantee safety, but does nothing about the other half of correctness, specifically liveness. [0]
Linear types (like in Austral [1] and Vale's higher RAII [2]) can help guarantee liveness, but we still have further to go.
Both are based on single-ownership (in the C++ sense) like Rust, which introduces errors that e.g. Haskell would not.
But even Haskell (and LiquidHaskell which has linear types) don't go far enough; Coq goes even further.
So yes, like you say, we have a long way to go w.r.t. correctness, even past the borrow checker though it is a big step forward.
To my original point though, even all of these tools put together will put restrictions on a program such that it sometimes won't be allowed to take the most optimal approach. Perhaps someday we'll get there!
[0] https://en.wikipedia.org/wiki/Safety_and_liveness_properties