Safe Made Easy Pt.1: Single Ownership is (Not) Optional
33 points by ergeysay
33 points by ergeysay
A directed acyclic graph, where a node can have several incoming edges, but you somehow can guarantee absence of cycles. […] I honestly have no idea if there are any languages exhibiting this mode.
This is Rust with refcounting, Rc and Arc etc.
So far this looks like an interesting variant of Rust’s borrow checker. It makes sense to integrate borrowing into the type system more explicitly.
I’m unsure from the descriptions which (if any) of the special types are implemented in the library and which are builtin language features. And I wonder if “dependencies” are exactly like Rust’s borrows, or if not, how they differ.
This is Rust with refcounting, Rc and Arc etc.
Pretty sure Rc/Arc don't guarantee absence of cycles? The fact you could make cycles with them was (part of?) the impetus for the Leakpocalypse, after all.
The "widening" approach in this article seems interesting, and not something I've seen before (I guess this is a thing in typescript? I've never written any typescript). I can't tell just from reading the article whether this is "magic" or a "footgun" or maybe both.
The "widening" approach in this article seems interesting, and not something I've seen before (I guess this is a thing in typescript? I've never written any typescript). I can't tell just from reading the article whether this is "magic" or a "footgun" or maybe both.
It's standard abstract interpretation per Cousot & Cousot '77, though I took some liberties with terminology (what I call "widening" is strictly the lattice join).
As someone also interested in this space, I would've found it helpful for the pt 2 post if you spelled out the type signatures for the functions and how exactly the the tracking for "what has been pushed to this array" works across function boundaries.
You also gave an example of a record where a field may be potentially reference another field, how does that work across function boundaries, where code may want to reason about aliasing? E.g. in Rust, std::mem::swap takes two mutable references so the implementation can rely on them not aliasing.
This is the subject of the next post, and I'd like to avoid spoiling it too much. Rust's approach is beautiful in its simplicity, but I wanted something less restrictive, so in my model two arguments can have arbitrary aliasing, which in turn necessitates polyvariant analysis.
Symbolic execution, linear types, dependent types, lots to chew on! Saving this for a closer read.
Thanks! Let me know what you think when you finish. Also, it's abstract interpretation (overapproximating) and not really true dependent types - just a vaguely similar kind of thing.