Alan Jeffrey, Mozilla Research
Systems programming language.
Hack without fear!
Safety guarantees based on two 1990s ideas:
Nothing can be included in Rust that isn't at least a decade old.
— Graydon Hoare, Rust founder.
Got water
and flowers
Got water
and flowers
and a friend who will barter flowers for cigarettes
Got water
and flowers
and a friend who will barter flowers for cigarettes
...later...
Got water
and cigarettes
water
⊗ flowers
⊗ (flowers ⊸ cigarettes)
⊢
water
⊗ cigarettes
water
⊗ flowers
⊗ (flowers ⊸ cigarettes)
⊢
water
⊗ cigarettes
water
⊗ flowers
⊗ (flowers ⊸ cigarettes)
⊢
water
⊗ cigarettes
models a friend who barters once and then vanishes
water
⊗ flowers
⊗ !(flowers ⊸ cigarettes)
⊢
water
⊗ cigarettes
⊗ !(flowers ⊸ cigarettes)
models a friend who barters as much as you like
LL does not have weakening (discard) or contraction (copy):
A ⊬ A ⊬ A ⊗ A
but recovers them for banged formulae:
!A ⊢ !A ⊢ !A ⊗ !A
Curry-Howard (constructive logic):
propositions are types,
proofs are typed programs
Gang of Four (constructive linear logic):
propositions are linear types,
proofs are linearly typed programs
Mutating in-place is attractive:
Mutating in-place has problems:
Linear types make this simpler.
Model in-place mutation by consuming the old value
and producing a new one: A ⊸ A
This is call-by-value-return.
Solution: use call-by-reference rather than call-by-value-result.
Rust has two reference types:
References are borrowed: if v : A then &v : &A (ditto &mut).
Rather than (A ⊗ B) ⊸ (A ⊗ C),
mutating functions have type (&mut A ⊗ B) ⊸ C.
But why is this sound?
Rust reference types actually carry lifetimes:
Functions are lifetime-polymorphic.
Lifetime inference usually allows lifetimes to be omitted.
Rust lifetimes are very similar to Tofte-Talpin regions:
There are some differences: