Rust for Semanticists

Rust for Semanticists

Rust

Rust

Rust

rust-lang.org A few of the >1400 Rust contributors

Rust

rust-lang.org

Rust

rust-lang.org

Rust

rust-lang.org

Rust

Systems programming language.

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

Hack without fear!

Rust

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.

Linear types

Linear logic

rust-lang.org Jean-Yves Girard, Linear logic, Theoretical Computer Science 50(1), 1987.

Linear logic

rust-lang.org

Got water
and flowers

Linear logic

rust-lang.org

Got water
and flowers
and a friend who will barter flowers for cigarettes

Linear logic

rust-lang.org

Got water
and flowers
and a friend who will barter flowers for cigarettes
...later...
Got water
and cigarettes

Linear logic

rust-lang.org

water
flowers
⊗ (flowerscigarettes)

water
cigarettes

Linear logic

waterflowers ⊗ (flowerscigarettes)

watercigarettes

Linear logic

waterflowers ⊗ (flowerscigarettes)

watercigarettes

models a friend who barters once and then vanishes

Linear logic

waterflowers ⊗ !(flowerscigarettes)

watercigarettes ⊗ !(flowerscigarettes)

models a friend who barters as much as you like

Linear logic

LL does not have weakening (discard) or contraction (copy):

A ⊬           AAA

but recovers them for banged formulae:

!A ⊢           !A ⊢ !A ⊗ !A

Linear types

rust-lang.org Gavin Bierman, Valeria de Paiva, Martin Hyland (seated) and Nick Benton, A Term Calculus for Intuitionistic Linear Logic, Proc. TLCA, 1993

Linear types

rust-lang.org

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

Linear types

rust-lang.org

Linear types

rust-lang.org

Linear types

rust-lang.org

Linear types

rust-lang.org

Mutable References

Mutation

Mutating in-place is attractive:

  • Less copying.
  • Existing APIs use it.

Mutation

Mutating in-place has problems:

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

Mutation

Linear types make this simpler.

Model in-place mutation by consuming the old value
and producing a new one: AA

This is call-by-value-return.

Mutation

rust-lang.org

Mutation

rust-lang.org Problem 1: doesn't scale well with multiple arguments.

Mutation

rust-lang.org Problem 2: doesn't cope with arguments that aren't mutated, so can be aliased.

References

Solution: use call-by-reference rather than call-by-value-result.

References

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 (AB) ⊸ (AC),
mutating functions have type (&mut AB) ⊸ C.

References

rust-lang.org

References

But why is this sound?

Region-based
memory management

Region-based memory management

rust-lang.org Mads Tofte and Jean-Pierre Talpin, Implementation of the typed call-by-value λ-calculus using a stack of regions, Proc. PoPL, 1994

Region-based memory management

rust-lang.org Problem: this program suffers from use-after-free.

Region-based memory management

rust-lang.org Problem: this program suffers from use-after-free.

Region-based memory management

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.

Region-based memory management

rust-lang.org Example after lifetime inference.

Region-based memory management

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.

Servo

Servo

rust-lang.org Map of the >500 Servo contributors

Servo

  • 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?

Servo

Lessons Learned

Lessons learned

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

Thanks

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