Aquascope: Improving Ownership Understanding with Datalog, Compilers, and Diagrams

November 25 2024 - 19:00+01:00

Modern programming languages have increased in complexity. Although type systems provide desirable program guarantees, such as Rust’s beloved ownership types, complex type systems introduce higher cognitive load upfront before developers get executable code. We’ve heard that ownership is difficult to understand, but how can we get developers capably programming in Rust, and later, how can we get them to use more advanced tools like verifiers and proof assistants?

In this talk I will deconstruct why developers struggle to understand Rust ownership and show the evolution of Aquascope, a tool that automatically generates diagrams of Rust’s runtime and compile-time semantics. We will look at the program analysis at the core of Aquascope’s permissions-based ownership model, and discuss how compiler architecture can facilitate (or impede) third-party tools like Aquascope.

Lastly, I will discuss how these techniques can be applied to other domains with complex information, such as verification. We want to empower developers to use our tools, not leave them cursing and walking away.

Presenter: Gavin is a PhD student and member of the Cognitive Engineering Lab at Brown University.

Meeting Link: Zoom Link

Recording Link: TBA