verdagon

Hi, article's author here (Verdagon, Vale's creator), and no, I'm just writing about someone else's language (Ante) that I thought was interesting.

Ante is making some very intriguing steps forward in memory safety design and I thought others would find it interesting too.

I'm often skeptical of the desire to create a lot of passes. In the early Vale compiler, and in the Mojo compiler, we were paying a lot of interest on tech debt because features were put in the wrong pass. We often incurred more complexity trying to make a concept work across passes than we would have had in fewer, larger passes. I imagine this also has analogies to microservices in some way. Maybe other compiler people can weigh in here on the correct number/kind of passes.

This approach solves one borrow checking pain point (by allowing temporary mutable aliasing, even across function boundaries), but the post might actually be a bit conservative in saying it will influence our programs' data to look like trees.

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!

Big fan of Verona, I love their memory safety approach as well. I wrote a bit about it in the Grimoire [0] too. IIRC they plan for the user to specify whether a region is backed by an arena allocator or GC, which sounds pretty nice. It's kind of hard to track down details though, most of my knowledge comes from reading David Chisnall's comments on lobste.rs.

[0] https://verdagon.dev/grimoire/grimoire

Yep, adding or removing an element would invalidate existing pointers to any other element in the hash table. This is generally regarded as a good thing if your elements are stored contiguously in the hash table, because a resize would cause any existing pointers to dangle. This should be true for C, and might be true for C# if you're using `struct`s which put the data inline (memory's a bit fuzzy on C#'s rules for references to structs though, maybe someone can chime in).

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.)

Great question! That's a big enough topic that I'd love to write a followup post about it. There's also a good thread on r/Compilers at https://www.reddit.com/r/Compilers/comments/1n2ay7g/comment/... about how Nick's model should support that.

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...

Hey all, this is a post explaining a new memory safety model by my friend Nick Smith (original proposal at https://gist.github.com/nmsmith/cdaa94aa74e8e0611221e65db8e4...)

It was interesting enough that I knew I had to write a post about it. Happy to answer any questions!

Great point =) That's true for a lot of languages (including Mojo too), so I should have said "non-owning reference" there. I'll update the post to clarify. Thanks for catching that!

I can imagine a Rust-like language where we have move-constructors (in TFA), and every generated Future subtype is opaque and also heap allocated for us.

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).

Good to see some more uses of linear types! Very few languages can use linear types, and their potential is huge IMO.

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...

I've been looking into this, and I suspect that one actually needs surprisingly little to interoperate safely with Rust.

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

Just did, thanks for the suggestion!

Thanks! And yeah I get that a lot >_> You're always welcome to swing by the discord where I can give a less arcane explanation! (https://discord.gg/SNB8yGH)

Hah I like this one!

PS. Congrats! https://verdagon.dev/blog/easter-egg-notes

It could, but then that List would have to be linear itself, and then the program would make sure that you eventually drain the list and destroy each element.

(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)

A really good question. In short, a linear List (or array, or hash map, etc) will only have two available destroyer functions:

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.

I've got some weird plans for variants. Basically, we'd represent an enum as a non-heap-allocated sealed interface with a struct for each "case". Basically, think of a Scala case class. Then, depending on where we put it (heap vs local/member/element), it will be compiled differently (a traditional interface vs a tagged variant, respectively). ...I don't expect that to make any sense.

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!

Almost, but see the replies to IcyWindows' comment for why this unfortunately doesn't work in C++. Also, I would love it if C++ had a way to actually move. That would unlock all sorts of interesting possibilities.

You're exactly right, and that's kind of what Vale's `destruct` is, if you squint.

They almost work like this. std::move doesn't actually move an object; it leaves an intact instance... which we still don't know how to destroy (because its destructor is private). This also means that if we have an e.g. Outer struct whose constructor takes some kind of linear type, that Outer has no way to ever relinquish it again, which is a prerequisite of all those desirable linear type / higher RAII patterns.

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)

There are a couple technical reasons:

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!

I'm glad you brought inheritance up! This rule has solved it nicely in my experience: if a struct is linear, then it can only inherit linear interfaces. And implementation inheritance works because it's really just a combination of interface inheritance + composition + method forwarding, none of which seem to have any particular trouble with linear types.

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!

Thank you, my friend =) So glad to hear you enjoy the articles!

Cool to see this on HN!

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.

Perhaps. The problem space's difficulty can bring some inherent complexity, yes... but I often hear that fact used to justify adding complexity that isn't actually necessary.

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 PumpkinOS project is pretty incredible. I can't imagine how much effort it would take to be compatible with all the system calls that the average Palm app would expect. I remember Palm did some truly weird things with memory: anything moderately large would need to be put into a special memory block that the OS could rearrange at will, and one would need to lock the block's handle to keep it stable while accessing it. Stuff like that must have been challenging (and fun) to implement in PumpkinOS.

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.

It makes me wonder if there are any language constructs that can make this a reasonable feature. One idea I've been tossing around is having the ability to roll back any changes to mutex-guarded data if an exception drops a mutex guard. It should be possible with the right language constructs and bookkeeping.

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.

Why's that?

I made no assumption like that, though do let me know if I've said something that could be interpreted that way.

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

[1] https://austral-lang.org/linear-types

[2] https://verdagon.dev/blog/higher-raii-7drl

I don't think the article made that conclusion? I see this in there:

As seen in the benchmarks, the current Rust standard library unstable sort implementation outperforms the C++ standard library counterparts

And I can't find any generalizations like that from the author, though I may have missed it.