February 10, 2023
The success of Rust has spurred the development of substructural features in higher-level languages (e.g., Scala, OCaml, D, Swift), offering tremendous potential for safe low-level memory management and controlling resources/capabilities. However, adapting Rust techniques to higher-level settings has been difficult due to conflicts with effects, higher-order functions, polymorphic types, and other forms of abstraction.
The recent reachability types proposal [1,2] based on a versatile and scalable substrate inspired by separation logic, promises to remove these obstacles and make lifetimes and sharing an integral part of mainstream high-level programming. This talk will give a tour of the initial proposal [1] and present an ongoing effort to smoothly scale the system to polymorphism and data types in the new lambda-diamond and F-sub-diamond calculi.
[1] https://dl.acm.org/doi/10.1145/3485516 [2] https://github.com/TiarkRompf/reachability
About Oliver
I am a temporary worker on a poultry farm. I am also fond of feeding software engineers with 1990s PL tech. Sometimes, I just don’t feel like popping the stack.