Noether: Symmetry in Programming Language Design

In this talk I'm going to argue for the importance of symmetry as a way of imposing helpful structure and regularity on programming languages. We say that something has a symmetry when it remains similar under transformation. A wide range of desirable properties of programming languages can be expressed as symmetry properties.

By focussing on symmetry in language design, we can improve a language's support for writing secure, robust and efficient programs. Noether is an experimental programming language design that I'm developing to explore this approach. It is structured as a series of layers, with inner layers satisfying strong symmetries that make programs easier to reason about. Outer layers satisfy fewer symmetries, but are more expressive. The layers are enforced by a type inference system.

Noether strictly follows the object-capability security model. This makes it possible to define patterns of cooperation between mutually untrusting components, to limit the scope for exploitation of bugs, and to minimize the amount of code that needs to be closely reviewed for security flaws. Techniques modelled on those used in capability-based operating systems are also employed to allow precise control over resource consumption. This mitigates the effects of accidental memory leaks and runaway buggy code, and can be used to defend against denial of service attacks from untrusted code and data sources.

Several concurrency models are supported, including declarative and event-loop concurrency. Parallelism is also supported, but separately from concurrency. This approach, using ideas from the Cilk and Cilk Plus languages and more recent languages such as Parasail, allows exploiting hardware parallelism without paying the complexity cost of concurrency except where it is needed. The language is pervasively transactional: every synchronous procedure call acts as a transaction that can be rolled back if an error occurs, automatically preserving the strong exception safety guarantee. The design also supports a distributed object model that can automatically and transparently recover from detected machine, process, and communication failures, but allows explicitly programmed handling of failures where necessary.

This talk will give an overview of the language, concentrating on new ideas, and some old but neglected ideas. It will describe the symmetries that hold at each layer of the language, and how these facilitate analysis of Noether programs for security and robustness. Along the way it will touch briefly on how transaction rollback and the distribution protocol can be implemented efficiently, making these ideas practical.

Actual implementation of the language is in the early stages -- you can help!

Daira Hopwood

Jacaranda Software, contracting for LeastAuthority.com

Daira Hopwood works on cloud storage systems for LeastAuthority.com. Ze has a long-standing interest in programming language research and security, and after 20 years has finally turned that into a concrete language design. Daira is transgender and was previously known as David-Sarah Hopwood.

Strange Loop

2009 - 2023

St. Louis, MO