What is a “non linear logic” or a “non linear problem “ in this context?
What is a “non linear logic” or a “non linear problem “ in this context?
In the case of these fancier data structures, it is perhaps also worth pointing out that many of them actually do follow ownership semantics, down to things like allowing shared access to multiple nodes, or exclusive access to a single node, so that no runtime checks are necessary. This is where I think the original article severely missteps in calling it a fatal flaw—because people are successfully building safe ownership-oriented abstractions using unsafe code. That’s a super-important capability of Rust.
To put it in my own words, and bear in mind that the last time I've worked with linear logic was 15 years ago. A linear logic restricts how often you are allowed to use a proposition in a derviation or proof tree.
The borrow checker is more like a linear type system. In linear type systems you restrict how often an identifier of a linear typed variable may be used. See, e.g. Phil Wadler's paper "Linear types can change the world", where he explores the idea to use linear types as an alternative to model the World(tm) in pure functional programming, i.e. an alternative to the IO monad.