Fearless concurrency with Rust

Fearless concurrency with Rust
blog.rust-lang.org

> 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).

(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?"

"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."