Refinement Types for Rust

Ranjit Jhala

Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable knob with which to inform the type system about invariants and correctness properties should be checked on the code. We will show how refinements can work hand in glove with Rust's ownership mechanisms to yield ergonomic type-based verification systems code.

The Human Factors of Formal Methods

Shriram Krishamurthi

"Formal methods" include specification, programming, and more: from logics to express to desired program behavior to algorithms to check correctness. Lean is a formal method, SMT is a formal method, LTL is a formal method, Rust's type system is a formal method. As formal methods improve in expressiveness and power, they create new opportunities for non-expert adoption. In principle, formal tools are now powerful enough to enable developers to scalably validate realistic systems artifacts without extensive formal training. However, realizing this potential for adoption requires attention to not only the technical but also the human side—which has received extraordinarily little attention from formal-methods research. This presentation presents some of our efforts to address this paucity. We apply ideas from cognitive science, human-factors research, and education theory to improve the usability of formal methods. Along the way, we find misconceptions suffered by users, how technically appealing designs that experts may value may fail to help, and how our tools may even mislead users.

OCamlFDO: Feedback-Directed Optimizer for OCaml

Static zero-alloc checker for OCaml

Greta Yorsh

Building programming languages for memory-safe hardware.

People who are serious about software should build their own hardware

David Chisnall

CHERI and similar systems provide a much stronger set of guarantees for languages to rely on, such as trapping out-of-bounds accesses and so on. At the same time, they disallow intrinsically unsafe operations, such as materialising pointers from thin air. CHERI was designed to be able to support a C abstract machine but it also provides a rich set of tools for language designers and implementers, which this talk will discuss. In the 1960s and '70s, computers came with a wide variety of abstract machines. The Burroughs Large Systems series implemented type-based tagging and hardware-assisted GC that allowed the entire OS to be written in a garbage-collected Algol dialect. Various Lisp machines accelerated different language-specific operations. The Intel APχ432 accelerated Ada (very badly, as a result of taping out the CPU before talking to the compiler team). But by the mid '80s, The C / PDP-11 abstract machine was the dominant abstraction. Processor vendors competed build faster and faster PDP-11s. This led to a feedback cycle. Fast processors were ones that ran code written in C-like languages quickly. Programs that needed performance used C-like languages, driving processor vendors to optimise for these workloads. Around 2007, process technology hit the end of Dennard Scaling, which made smaller transistors both faster and lower power. Since then, CPUs have continued to improve performance, but much more slowly. Real performance wins have come from accelerators, where there's a much tighter coupling between language and hardware designs. This presents an opportunity for language designers to build things that can work on current hardware but which could be significantly accelerated by alternate designs. This talk will discuss how researchers can build prototype hardware and engage with hardware vendors to build languages for the next 50 years.

The Virtualized Labours of Hercules: Strengthening the Security of Modern Language Runtimes

Jeremy Singer

Just as the mythical Hercules grappled with foes on multiple fronts, today's programming language runtimes face relentless attacks from a variety of malicious actors. This presentation explores the diverse attack surfaces that modern runtimes expose, considering effective strategies for mitigating these risks in real-world systems. We'll examine key trends in micro-architecture, such as tagged pointers and trusted execution environments, demonstrating how these innovations can be harnessed by language runtimes to deliver enhanced security. Many of our insights are drawn from research conducted on CHERI platforms as part of the Capable VMs project. Looking ahead, we'll speculate on the evolution of processor design and how future hardware might incorporate advanced security mechanisms. From a language implementation standpoint, we will discuss how these developments could transform the landscape of future runtime security.

Generating correct code for your programmers

Hila Peleg

Programming systems deserve a theory too!

Tomas Petricek

We know how to study programming languages, but programs are created not just by writing code. They are created by interacting with rich, stateful programming systems and environments. Programming systems still involve code, but they also include live previews, structure editors, debugging tools, runtime environments and other developer tools. If we want to make programming easier, more accessible and more flexible, we should shift our attention from programming languages to programming systems! In this tutorial, I will introduce different research methods that can be used for studying programming systems. We will look at interesting characteristics of past programming systems that were lost in history, look how to adapt formalisms familiar from programming languages to study interactive systems and also explore what a research implementations of small programming system can teach us! Throughout the tutorial, you will encounter a variety of systems ranging from modern IDEs and Jupyter Notebooks to Smalltalk and Commodore 64 BASIC.