The Game Semantics of the Rust Programming Language

This project falls into the EPSRC Programming Languages and Compilers research area.

Rust is a modern systems programming language which is designed as an alternative to popular languages like C++. Systems programming demands high-performance code, and a language able to interact with the hardware easily. At the same time, Rust tries to meet demands for safety, which is that any program which compiles is well behaved, such as freeing memory which is not longer needed.

Memory safe languages often incorporate a feature called a garbage collection, which runs alongside the user's program to free unused memory. This, unsurprisingly, leads to poor performance, and so Rust avoids this by having an advanced typing system which tracks who 'owns' values in the program, so they can be identified as unused. To handle cases where this system is too restrictive to solve the problem, Rust offers an 'unsafe' construct, which puts the burden on the program to prove that their code is safe.

The key objective of this project is to understand the semantics of the Rust language through the lens of game semantics. The semantics of a programming language gives a mathematical meaning to programs written in that language. Game semantics is a style based on the idea that a part of a program (a term) can be modelled as a strategy in a game of question and answer it plays with its environment.

Over the last 25-years, game semantics has proven to be a powerful paradigm, providing results for languages with many diverse features. Game semantics for Rust have yet to be explored, and so this project will investigate how the 'ownership' system of Rust manifests itself in the strategies of terms. To reason about programs using the 'unsafe' construct, we will need to explicitly handle in strategies notions like uninitialized values or dangling pointers.

This is a another novelty of our research methodology, as the abstract languages game semantics is normally used for are safe. One of the techniques we intend to use is operational game semantics, which has only been explored in the sequential setting. Handling concurrency in Rust would motivate generalising this technique, which will also be applicable outside of Rust.

With a semantic model at hand, we can then turn our attention to the next aim - developing reasoning techniques exploiting this model. A canonical problem in semantics is contextual equivalence - essentially asking if one term can be substituted for another everywhere. Game semantics has been used to solve this problem in a variety of settings, and should yield satisfying results here.

Another type of problem is that of verification - proving that a program satisfies a particular property. A natural instance of this arises in Rust from showing that code in an 'unsafe' construct is in fact safe. Recent work on Rust has established a technique to generate conditions a library using 'unsafe' must meet in order to be safe, and provides a framework for conducting these proofs.

However, developing these proofs still requires skilled human intervention, making them impractical for widespread use. Techniques exploiting game semantics have produced automatic methods for program verification in other settings, and so it is hoped the same will be the case here. Achieving this would involve a novel investigation of how satisfying these logically defined conditions constrain the strategies of terms, bringing together ideas from different areas of semantics.

Once sound mathematical techniques have been devised for reasoning about Rust programs, these can be applied to create practical tools for verification problems. A final aim of this project is to produce prototype tools based upon these techniques, and assess their efficiency on representative instances. It is likely that other languages seeking to balance performance with safety, such as Carbon, will adopt a similar techniques to Rust, making this work more widely applicable.