Nature has beautiful forms: from the crescent waves on the ocean to the beautiful wings of certain butterflies; from the stripes and spots of animals to the branching and weaving of plants and trees.

All these patterns seem intricate and complex. Often they can be modeled in a simple and effective way. Sometimes this model lets you learn something about nature.

In this workshop, we will explore Lindenmayer systems, or L-systems. These systems allow you to model various natural forms such as plants, trees and certain algae. Furthermore, it offers a playground for certain type of fractals. We will not only play with L-systems, we will also learn techniques for expressing and rendering them. It is these techniques that will transit from the pleasant playground of the workshop into the toolbelt of the participant.

So come and learn how to model your favourite forms of nature.

Rust 2018 brought with it “non-lexical lifetimes” (NLL), a big overhaul of how the borrow checker worked that allowed it to accept a lot more programs. And yet, we’re still not accepting the full range of programs that was envisioned by the original NLL RFC – this is both for performance reasons and because the formulation didn’t turn out to be as flexible as originally thought.

Polonius is a “reframing” of Rust’s borrow checker. It works quite differently than the original system. Rather than tracking how long each reference is used (its “lifetime”), it tracks where each reference may have come from (its “origin”) – and it does so in a very fine-grained way. As a result, Polonius is able to accept all the programs that the NLL RFC envisioned, and a few more! We also believe it can be made more performant (though that has yet to be fully proven out).

This talk will explain how Polonius works in a simple and example-driven style. It will help you to gain a deeper understanding of how Rust’s borrow checker works internally.

Rust really hits a sweet spot with respect to programming languages on account of a) its usefulness when working at a low level, coupled with b) its style of type system. Because of a), Rust can be — and is — used in places which tend to safety-critical: cyber-physical systems, autonomous vehicle infrastructure, robotics, etc. When building systems for these safety-critical environments, one also often formally proves properties about their software. That’s where b) comes in.

Rust’s type system is borne from the same ilk as those used in proof assistants like Agda, Coq, or Lean. Because of this, we can use Rust’s type system in similar ways we’d use a proof assistant to produce safer and more correct programs. This is envisioned by reducing the language of these disparate systems into the lingua franca of type theory.

This talk will explore using (and abusing) Rust’s type system to mimic the proofs one writes about their Rust programs while also enumerating how this mimicry is derived from common ground in the worlds of types or categories.

Have you ever wondered why you can’t look up a character in a string by its index?

    let hello = String::from("world");
    println!("{}", hello[0]);
                   ^^^^^^^^ `std::string::String` cannot be indexed by `{integer}`

Or why the length of a String can be wildly different from the number of characters in the string?

    let rust = String::from("錆");
    println!("{}", rust.len()); => 3
    println!("{}", rust.chars().count()); => 1

In this talk we’ll dive into unicode by looking at how Kanji is represented in Rust. You’ll learn about things like the Han unification, the origins of CJK languages from Oracle bone script, and why Rust handles Strings differently than we expect.