HN

Comments (12)

• sirwhinesalot
  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...
• Menu

  verdagon
  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!
• Menu

  Animats
  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.
• gdotdesign
  This reminded me of the Vine programming languages inverse operator https://vine.dev/docs/features/inverse
• gnarlouse
  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!
• Menu

  CoalitionOfPity
  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.
• deakmisra
  [flagged]