Against Borrowing: Own the forest, not the trees!
Rust’s version of an ownership type system (the “borrow checker”) is hard for programmers to understand; the semantics are difficult for theorists to model; and in spite of this complexity and difficulty, many important data structures, including B-trees, polygon meshes, winged-edges, and even the relatively humble doubly-linked list, cannot be implemented straightforwardly in memory-safe Rust.
In this talk I’ll try to show how Rust-style Ownership Types can be modelled on top of the foundation of classical Object-Oriented Ownership Types. Focusing on Ownership, rather than Borrowing, means we can think about the forest, not the individual trees — even if the trees end up walking around the forest from time to time. I hope Treating Rust Ownership as Ownership Types offers a simpler conceptual model for novices; a more straightforward forjmal treatment for theorists; a wider selection of safe linked structures for programmers; and perhaps even a foundation for the next generation of imperative programming language designs.
I’ll no doubt end up ranting about how building a Dafny program embodying Ownership has helped and hindered this effort. (work with Tobias Wrigstad, Sophia Drossopoulou, Suan Eisenbach, Michael Homer, Andrew Fawcett, etc)
James Noble (kjx@acm.org) is an independent creative researcher & programmer based in Wellington, New Zealand. After completing honours and doctoral degrees at Victoria University of Wellington (VUW), James worked at the University of Technology, Sydney, the Microsoft Research Institute at Macquarie University, and is recovering from a long stint as professor of computer science & software engineering at VUW.
James’s research centres around software design. This includes the design of the users’ interface, the parts of software that users have to deal with every day, and the programmers’ interface, the internal structures and organisations of software that programmers see only when they are designing, building, or modifying software.
James’s research in both of these areas is coloured by a longstanding interest in object-oriented approaches to design, and topics he has studied range from aliasing and object ownership, programming languages, design patterns, agile methodology, via usability, visualisation and computer music, to postmodernism and the semiotics of programming.
Tue 14 OctDisplayed time zone: Perth change
13:40 - 15:20 | |||
13:40 35mKeynote | Against Borrowing: Own the forest, not the trees! IWACO James Noble Independent. Wellington, NZ | ||
14:15 25mTalk | A Verified Thread-Safe Array in Rust IWACO Sasha Pak Australian National University, Fabian Muehlboeck Australian National University, Alex Potanin Australian National University | ||
14:40 25mTalk | Temporal Resource Typing: Enriching Substructural Typing for Liveness Reasoning IWACO | ||
15:05 25mTalk | Bringing Fearless Concurrency to Swift IWACO Mae Milano Princeton University | ||
