> the same tools that make Rust safe also help you tackle concurrency head-on.
The tools that make Rust safe, in this instance, being its ownership type system. Why on earth should that be the case? Why would ownership types make concurrency easier? The post gives plenty of in-depth answers to this question, but to my mind it misses the bigger picture.
The big-picture reason why ownership types and concurrency match so well is the Curry-Howard correspondence.
Ownership types are known as linear[1] types in the PL theory literature. Linear types are so-called because they correspond to linear logic, a logic sometimes described as "the logic of resources" rather than "a logic of truth". In linear logic, instead of reasoning about eternal truths like "1 + 1 = 2", you reason about resources, like "I have an apple and a banana". If you also happen to know that "from an apple, I can make applesauce", then linear logic lets you reason that you can obtain the state "I have applesauce, and a banana" (but no longer an apple).
However! Linear logic has another interpretation, a Curry-Howard interpretation. You can also view it as a type system for a concurrent language based on message-passing, where your types describe the protocols message-channels obey. "I have an apple and a banana" corresponds to a channel which will first produce an apple, then a banana, then close. This is known as the session-types interpretation[2].
At first glance it may seem that this interpretation of linear logic and Rust's interpretation are unconnected. I doubt it; in logic, everything connects to everything else. It's no coincidence, for example, that ownership (linearity) is what you need in order to send mutable values across a channel without copying. There is a deeper structure waiting here to be discovered, and I for one am deeply excited about it.
[1] In Rust's case, technically they are affine types. An affine type is a linear type whose values can be freely dropped, i.e. deallocated.
[2] Session types have been around for a long time, but only fairly recently was the connection to linear logic discovered.
For anyone interested in session types, we are currently working on implementing a library for them, in Rust[0]. However, as you point out, Rusts types are affine, not linear, so we're also working on a compiler plugin for Rust that let's you track protected types and make sure they aren't dropped, letting you sort of emulate linear types[1].
Most of this is still in a pretty early state (neither actually compile at the moment), and there are some fundamental problems with the plugin (it's impossible afaik for compiler plugins to examine external crates), but someone might find it interesting.
Eventually, our goal is to use these tools to solve some concurrency problems in Servo.
"First, the `linear` attribute as described here does not create true `linear` types: when unwinding past a `linear` type, the `linear` attribute will be ignored, and a `Finalize` trait could be invoked. Supporting unwinding means that Rust's linear types would in effect still be affine."
Ownership is doable in a dynamic language, provided you are willing to tolerate aborts: C++'s std::unique_ptr is enforced at runtime. Similarly, you can emulate dynamic borrowing using something like Rust's RefCell, which aborts when you attempt to mutably borrow a value twice (though it can be quite difficult to reason about from a usability perspective).
But if you're building on top of F# you have a static type system at your disposal. Usually, languages that incorporate linear types and first-class garbage collection treat linear types as a separate kind, and allow them to interact with standard types only in limited ways. See, for example, https://github.com/idris-lang/Idris-dev/wiki/Uniqueness-Type.... I believe http://protz.github.io/mezzo/ is also exploring this design space.
My lang will have a static type, so that info is usefull.
It will start as a interpreter, but probably the challenge is the ergonomics of it: How make it "easier" to use... probably limit it to only handle resources? (ie: files, handles, etc, like the IDisposable in .net)
(search for { contra godel, direct logic }) Can't find it but he quotes a really interesting exchange between Wittgenstein and Turing (who was attending his class) where W in his inimitable style just waves away paradoxes and says "so what?"
> the same tools that make Rust safe also help you tackle concurrency head-on.
The tools that make Rust safe, in this instance, being its ownership type system. Why on earth should that be the case? Why would ownership types make concurrency easier? The post gives plenty of in-depth answers to this question, but to my mind it misses the bigger picture.
The big-picture reason why ownership types and concurrency match so well is the Curry-Howard correspondence.
Ownership types are known as linear[1] types in the PL theory literature. Linear types are so-called because they correspond to linear logic, a logic sometimes described as "the logic of resources" rather than "a logic of truth". In linear logic, instead of reasoning about eternal truths like "1 + 1 = 2", you reason about resources, like "I have an apple and a banana". If you also happen to know that "from an apple, I can make applesauce", then linear logic lets you reason that you can obtain the state "I have applesauce, and a banana" (but no longer an apple).
However! Linear logic has another interpretation, a Curry-Howard interpretation. You can also view it as a type system for a concurrent language based on message-passing, where your types describe the protocols message-channels obey. "I have an apple and a banana" corresponds to a channel which will first produce an apple, then a banana, then close. This is known as the session-types interpretation[2].
At first glance it may seem that this interpretation of linear logic and Rust's interpretation are unconnected. I doubt it; in logic, everything connects to everything else. It's no coincidence, for example, that ownership (linearity) is what you need in order to send mutable values across a channel without copying. There is a deeper structure waiting here to be discovered, and I for one am deeply excited about it.
[1] In Rust's case, technically they are affine types. An affine type is a linear type whose values can be freely dropped, i.e. deallocated.
[2] Session types have been around for a long time, but only fairly recently was the connection to linear logic discovered.
Links/papers on session types:
1."Propositions as Sessions" by Wadler (http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-...)
2. Caíres and Pfenning, "Session types as intuitionistic linear propositions" (http://www.cs.cmu.edu/~fp/papers/concur10.pdf)
3. Pfenning's published works page (http://www.cs.cmu.edu/~fp/publications.html).