Rust for Semanticists

Systems programming language.

• Arrays without buffer overflow attacks.
• Manual memory management without segfaults.
• Threads without data races.

Hack without fear!

Safety guarantees based on two 1990s ideas:

• Linear types.
• Region-based memory management.

Nothing can be included in Rust that isn't at least a decade old.
    — Graydon Hoare, Rust founder.

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:

• Less copying.
• Existing APIs use it.

Mutating in-place has problems:

• Thread safety.
• Aliasing (e.g. simultaneously iterating and mutating a container).
• Semantics?

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:

• &A: a copyable reference to an immutable A.
• &mut A: a linear reference to a mutable A.

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:

• &α A: a copyable reference with lifetime α to an immutable A.
• &α mut A: a linear reference with lifetime α to a mutable A.

Functions are lifetime-polymorphic.

Lifetime inference usually allows lifetimes to be omitted.

Rust lifetimes are very similar to Tofte-Talpin regions:

• Lifetimes are nominal (gensym-like).
• Types and lifetimes are separate kinds.
• References are annotated with lifetimes.

There are some differences:

• Lifetimes do not form a stack.
• Lifetimes do not exist at run-time.

• Next generation web rendering engine.
• About 1 million Rust LoC, incluing about 250 dependencies.
• Mostly Rust, some C/C++ (Spidermonkey, openssl, ...)
• Some Rust code is unsafe or uses dynamic checks.
• No buffer overflows in safe Rust code.
• The largest linearly typed program in the world?

• Linear types and region analysis scale up.
• People care about safety+efficiency (most loved technology).
• It often takes 20 years for research to get into production.
• “Industrially relevant” research is not always the most relevant to industry.

• Me: Alan Jeffrey
• Rust: https://rust-lang.org/
• Playground: https://play.rust-lang.org/
• Servo: https://servo.org/