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.
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.
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.
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!
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.
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.
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.
"Just" make verification faster. ;)