Figuring out how to make this was a pretty wild ride. I had zero clue how to approach this, so I went into the mountains with pencil and paper until I figured something out.
I started with a sort of "compile-time generational references" approach, where every reference would also remember when it was made, at compile-time. Then that evolved into a couple more things until I finally figured out this reverse approach. We'll see if it sticks.
Seems to me you did what any engineer worth his salt would do: sit down and look at the underlying mechanisms, to map the problem, and then highly efficient solutions present themselves. It's amazing to me no one seems to have done this before.
That raises the question why did Rust pivot to lifetimes? It was a bias towards theory? Or they just missed the simplication of their model? So they exited the problem space too early, happy to have found a solution?
I sure am happy to see this non-dogmatic thinking, many blessings are to come of it. It seems we are getting closer to the "final language", and languages become a solved problem.
> Seems to me you did what any engineer worth his salt would do: sit down and look at the underlying mechanisms, to map the problem, and then highly efficient solutions present themselves.
Truer words were never spoken.
> It's amazing to me no one seems to have done this before.
You would be surprised how many valuable problems and solutions have not been solved by anyone before. Apparently, it happens to be the norm in the wild. My understanding is that it's about how far one is willing to strive for an ideal.
> It seems we are getting closer to the "final language", and languages become a solved problem.
A final language? I like the sound of it. No more picking complexity, latency, simplicity, expressiveness, portability and other tradeoffs.
> > It seems we are getting closer to the "final language", and languages become a solved problem.
>
> A final language? I like the sound of it. No more picking complexity, latency, simplicity, expressiveness, portability and other tradeoffs.
This sound to me like havin a single tool. Only a hammer and every problem looks like a nail...
Out of curiosity, have you looked into capture checking from Scala? It's proposed as a generalization of the rust borrow checker, to handle capabilities and other side-effectful computations (error handling, asynchrony, ...) in an ergonomic manner. Not sure if/how much cross-pollination there might be :-)
A lot of developer rituals can be avoided for obvious cases (of multiple writes to the same variable) leading to clean code. Your Valen looks promising.
I learnt, while reading your blogs, that rustc can run embedded - which might come in handy for one of our projects, Craft, for embedded compiling + uploading on mobile.
We have built arcc (architectural compiler/linter) which enforces architectural rules for correctness like strict CQRS separation and other 10+ architectural rules at compile time. Currently, arcc is for TypeScript/JS codebase. Future scope is on Rust codebases.
> Then that evolved into a couple more things until I finally figured out this reverse approach. We'll see if it sticks.
The way you phrased that sentence, something tells me that it sticks. Reading tea leaves: compressed in those sentences somewhere is an insight you have which you are damn sure of, while deliberately withholding it and thinking it through before you guarantee it yourself. Did my tea leaves fail me :).
In Hoare-type proof of correctness work, it's normal to work backwards from the proof goal (such as an assert statement) back upwards through the program, adding info about code that affects the variables in the assertion. This approach to borrow checking follows that model. You want some state at some point, and you work backwards to see if the preceding code gets you there. Makes a lot of sense for lifetimes.
The main problem with doing this inside a compiler is performance. You backtrack for each thing you need to prove, going through the same code more than once. I used to think that compilers should use more verification technology, but people start screaming about compile times.
Yes. That's the symbolic execution approach to verification. At each IF, there's another set of future paths to explore, with more constraints on the variables. The Microsoft Static Driver Verifier is said to work that way.[1] It's mostly automatic, but slow. It made OS crashes caused by Windows drivers mostly a thing of the past in Windows 7.
If I may make a suggestion, really try to avoid going the constraint route as in Rust's lifetime tracking.
It is a pain to ensure it works as intended. A simple syntax directed algorithm (even in reverse ;) ) is preferable if you can get away with it. I guess the compatibility with Rust will end up forcing you into the constraint route though.
Big props to the group borrowing idea. It is similar to my own attempts (including the use of an explicit path rather then some generic lifetime parameter), but I never got the rules quite this clear.
In the other article you mentioned stability. That's one part of the design I never quite figured out in a way I was happy with. It's not really mutation that matters, it is (potential) freeing.
If I have a very large struct made up of substructs, none of which is stored through a pointer, then mutating any part of this struct invalidates no references, it is the same as if each individual field was mutated. But I wanted to avoid needing an "invalidates" annotation of some sort...
Hey! What were you designing? I didn't know anyone was doing anything with explicit paths.
I think there's a way to make the invalidation annotation (like Valen's `mut`) work nicely and feel ergonomic. Carbon is also facing this particular challenge, they have a literal invalidate annotation too.
Hey, sorry for the late reply, no idea if you'll check this still on hackernews (though I do have you on discord so I can poke you there if need be ;) ).
I was experimenting with implementing something Hylo-like (formerly Val). Meaning no references what so ever, only parameter passing modes. But I hated their subscript mechanism (a form of coroutine, used to implement iterators and views, similar to what Graydon originally wanted for Rust).
I wanted to have what they call subscripts work as regular functions, so I needed some way for a function to return a reference-like thing. This gets you down the rabbit hole of extending second-class references until they're first-class.
Hylo already tracks paths implicitly in the function arguments, it needs to do so to maintain value semantics (if you have two references mutating the same thing, value semantics break). I wasn't particularly worried about the value semantics, what I wanted were nice to work with references. The first thing was how do you return a reference from a function in a way that is safe?
Well, if you apply the same rule as subscripts (that they can only appear as arguments to other functions, not assigned to variables), then everything just works out. The only thing I needed to know was what did the reference point to? Well, Hylo tracks paths, but I need to say which path, so I had something like the following:
// returns the longest slice of v1 that shares a prefix with v2
fun matching(in v1: Vec<int>, in v2: Vec<int>) -> &Slice<int> of v1
That `of v1` annotation essentially said "this reference has the same path as v1". I didn't give you a way to be more specific about the paths like you allow (I love that idea!), you could only be specific about which argument it was a reference of, and the path was inferred from that.
There were more complicated cases I could think of that required the thing after `of` to be a set:
// returns the longest of s1 or s2
// output must be conservative
fun longest(in s1: &Slice<int>, in s2: &Slice<int>) -> &Slice<int> of {v1, v2}
In this case the slice can be of either input and the compiler has to be conservative about it.
Once this was in place then it was a matter of expanding things where you could store Slices (and single element references) in variables, as long as they were in the same scope as their path, and where you could store Slices and Refs inside structs (which then become a view type as well, like C#'s ref structs).
I ended up getting frustrated with it and tapping out, but I'm glad there are people exploring this path route. It is much better IMO than abusing parametric polymorphism to track lifetimes.
I just wanted to take the time to compliment this note in your blog:
> My stance: if you want someone to take the time to read something, take the time to write it by hand.
Thank you! I pretty strongly believe this. If we take the time to write for each other, then the internet stays a place where humans connect with each other. Otherwise we get lost in the noise and it becomes a place where machines talk to each other through humans. Fingers crossed the world figures this out.
Figuring out how to make this was a pretty wild ride. I had zero clue how to approach this, so I went into the mountains with pencil and paper until I figured something out.
I started with a sort of "compile-time generational references" approach, where every reference would also remember when it was made, at compile-time. Then that evolved into a couple more things until I finally figured out this reverse approach. We'll see if it sticks.
Hope you all enjoy!
Seems to me you did what any engineer worth his salt would do: sit down and look at the underlying mechanisms, to map the problem, and then highly efficient solutions present themselves. It's amazing to me no one seems to have done this before.
That raises the question why did Rust pivot to lifetimes? It was a bias towards theory? Or they just missed the simplication of their model? So they exited the problem space too early, happy to have found a solution?
I sure am happy to see this non-dogmatic thinking, many blessings are to come of it. It seems we are getting closer to the "final language", and languages become a solved problem.
> why did Rust pivot to lifetimes
not sure if this is the reason, but imo it's a way to express this without requiring to know the implementation details of abstractions
> Seems to me you did what any engineer worth his salt would do: sit down and look at the underlying mechanisms, to map the problem, and then highly efficient solutions present themselves.
Truer words were never spoken.
> It's amazing to me no one seems to have done this before.
You would be surprised how many valuable problems and solutions have not been solved by anyone before. Apparently, it happens to be the norm in the wild. My understanding is that it's about how far one is willing to strive for an ideal.
> It seems we are getting closer to the "final language", and languages become a solved problem.
A final language? I like the sound of it. No more picking complexity, latency, simplicity, expressiveness, portability and other tradeoffs.
> > It seems we are getting closer to the "final language", and languages become a solved problem. > > A final language? I like the sound of it. No more picking complexity, latency, simplicity, expressiveness, portability and other tradeoffs.
This sound to me like havin a single tool. Only a hammer and every problem looks like a nail...
Exactly. The old wisdom may not be 100% true after all.
Composed of the right primitives at sufficient granularity, we may yet approach the one true hammer :)
Out of curiosity, have you looked into capture checking from Scala? It's proposed as a generalization of the rust borrow checker, to handle capabilities and other side-effectful computations (error handling, asynchrony, ...) in an ergonomic manner. Not sure if/how much cross-pollination there might be :-)
https://docs.scala-lang.org/scala3/reference/experimental/ca...
Looked around your blog. Awesome work.
A lot of developer rituals can be avoided for obvious cases (of multiple writes to the same variable) leading to clean code. Your Valen looks promising.
I learnt, while reading your blogs, that rustc can run embedded - which might come in handy for one of our projects, Craft, for embedded compiling + uploading on mobile.
We have built arcc (architectural compiler/linter) which enforces architectural rules for correctness like strict CQRS separation and other 10+ architectural rules at compile time. Currently, arcc is for TypeScript/JS codebase. Future scope is on Rust codebases.
> Then that evolved into a couple more things until I finally figured out this reverse approach. We'll see if it sticks.
The way you phrased that sentence, something tells me that it sticks. Reading tea leaves: compressed in those sentences somewhere is an insight you have which you are damn sure of, while deliberately withholding it and thinking it through before you guarantee it yourself. Did my tea leaves fail me :).
Interesting.
In Hoare-type proof of correctness work, it's normal to work backwards from the proof goal (such as an assert statement) back upwards through the program, adding info about code that affects the variables in the assertion. This approach to borrow checking follows that model. You want some state at some point, and you work backwards to see if the preceding code gets you there. Makes a lot of sense for lifetimes.
The main problem with doing this inside a compiler is performance. You backtrack for each thing you need to prove, going through the same code more than once. I used to think that compilers should use more verification technology, but people start screaming about compile times.
> I used to think that compilers should use more verification technology, but people start screaming about compile times.
"Just" make verification faster. ;)
Can it be optimized by doing it forward again, for all values at once?
Yes. That's the symbolic execution approach to verification. At each IF, there's another set of future paths to explore, with more constraints on the variables. The Microsoft Static Driver Verifier is said to work that way.[1] It's mostly automatic, but slow. It made OS crashes caused by Windows drivers mostly a thing of the past in Windows 7.
[1] https://www.microsoft.com/en-us/research/wp-content/uploads/...
If I may make a suggestion, really try to avoid going the constraint route as in Rust's lifetime tracking.
It is a pain to ensure it works as intended. A simple syntax directed algorithm (even in reverse ;) ) is preferable if you can get away with it. I guess the compatibility with Rust will end up forcing you into the constraint route though.
Big props to the group borrowing idea. It is similar to my own attempts (including the use of an explicit path rather then some generic lifetime parameter), but I never got the rules quite this clear.
In the other article you mentioned stability. That's one part of the design I never quite figured out in a way I was happy with. It's not really mutation that matters, it is (potential) freeing.
If I have a very large struct made up of substructs, none of which is stored through a pointer, then mutating any part of this struct invalidates no references, it is the same as if each individual field was mutated. But I wanted to avoid needing an "invalidates" annotation of some sort...
Hey! What were you designing? I didn't know anyone was doing anything with explicit paths.
I think there's a way to make the invalidation annotation (like Valen's `mut`) work nicely and feel ergonomic. Carbon is also facing this particular challenge, they have a literal invalidate annotation too.
Hey, sorry for the late reply, no idea if you'll check this still on hackernews (though I do have you on discord so I can poke you there if need be ;) ).
I was experimenting with implementing something Hylo-like (formerly Val). Meaning no references what so ever, only parameter passing modes. But I hated their subscript mechanism (a form of coroutine, used to implement iterators and views, similar to what Graydon originally wanted for Rust).
I wanted to have what they call subscripts work as regular functions, so I needed some way for a function to return a reference-like thing. This gets you down the rabbit hole of extending second-class references until they're first-class.
Hylo already tracks paths implicitly in the function arguments, it needs to do so to maintain value semantics (if you have two references mutating the same thing, value semantics break). I wasn't particularly worried about the value semantics, what I wanted were nice to work with references. The first thing was how do you return a reference from a function in a way that is safe?
Well, if you apply the same rule as subscripts (that they can only appear as arguments to other functions, not assigned to variables), then everything just works out. The only thing I needed to know was what did the reference point to? Well, Hylo tracks paths, but I need to say which path, so I had something like the following:
That `of v1` annotation essentially said "this reference has the same path as v1". I didn't give you a way to be more specific about the paths like you allow (I love that idea!), you could only be specific about which argument it was a reference of, and the path was inferred from that.There were more complicated cases I could think of that required the thing after `of` to be a set:
In this case the slice can be of either input and the compiler has to be conservative about it.Once this was in place then it was a matter of expanding things where you could store Slices (and single element references) in variables, as long as they were in the same scope as their path, and where you could store Slices and Refs inside structs (which then become a view type as well, like C#'s ref structs).
I ended up getting frustrated with it and tapping out, but I'm glad there are people exploring this path route. It is much better IMO than abusing parametric polymorphism to track lifetimes.
I have no help to offer, but as a bystander who loves Rust I am very hopeful good things come of this for you @verdagon!
This reminded me of the Vine programming languages inverse operator https://vine.dev/docs/features/inverse
I just wanted to take the time to compliment this note in your blog: > My stance: if you want someone to take the time to read something, take the time to write it by hand.
Thank you! I pretty strongly believe this. If we take the time to write for each other, then the internet stays a place where humans connect with each other. Otherwise we get lost in the noise and it becomes a place where machines talk to each other through humans. Fingers crossed the world figures this out.
[flagged]