Rust programs can still leak and deadlock

enum List { Nil, Cons(u32, Arc<Mutex<List>>) }

let x = Arc::new(Mutex::new(List::Nil));
*x.lock() = List::Cons(1, x.clone());
drop(x);   // refcount is 1: never freed

fn swap(x: &Mutex<u32>, y: &Mutex<u32>) {
    let mut gx = x.lock();
    let mut gy = y.lock();
    let tmp = *gx; *gx = *gy; *gy = tmp;
}
spawn(|| swap(x, y));
spawn(|| swap(y, x));

Both programs type-check.

Goal: type systems in which every well-typed program is free of deadlocks and leaks, with machine-checked proofs.

Prior work: session types

let c = fork(λc′.
    let (c′, n) = receive(c′) in
    let c′ = send(c′, n mod 2 == 0) in
    close(c′))
let c = send(c, 3) in
let (c, b) = receive(c) in
close(c)

Type-checked ⇒ no deadlocks and no leaks.

What was missing: a machine-checked proof.

Connectivity graphs: a proof method for session types

Connectivity graphsPOPL'22

Multiparty GVICFP'22

The same idea for locks

Higher-order leak and deadlock free locksPOPL'23, distinguished paper

Prior work: Actris

let (c1, c2) = new_chan () in
fork { let x = c2.recv() in
       c2.send(x + 2) };
c1.send(40);
let y = c1.recv() in
assert(y = 42)

{ c ↣ !(x:τ)⟨v⟩{P}. p ∗ P[t/x] }
    send c (v[t/x])
{ c ↣ p[t/x] }

Dependent session protocols in separation logic from first principlesICFP'23

LinearActris: deadlock freedom inside the logic

c1, d1 := new_chan()
c2, d2 := new_chan()
fork { c1.recv(); d2.send(2) }
c2.recv(); d1.send(3)

Deadlock-free separation logicPOPL'24

Probabilistic programming

h = rand(Normal(1.7, 0.5))
if rand(Bernoulli(0.5))
  observe(Normal(h, 0.1), 2.0)
end

h = rand(Normal(170, 50))
if rand(Bernoulli(0.5))
  observe(Normal(h, 10), 200)
end

Conditioning on an event of probability zero

Both programs give 1.70 m and 170 cm.

Exact inference by discretization

let x = gaussian(0, 1) in
…
if x < 0.8 then x < 0.1
           else x < 2.0

let x = discrete(0.5398, 0.2483,
                 0.1891, 0.0228) in
…
if x < 2 then x < 1
         else x < 3

Slice: type-directed discretization of probabilistic programsOOPSLA'26

Boa: one algorithm for many kinds of automata

Fast coalgebraic bisimilarity minimizationPOPL'23

Prior work: NetKAT

KATch: a fast symbolic verifier for NetKATPLDI'24

Packets with unbounded contents

push(v) · pop(v) ≡ 1
push(v) · pop(w) ≡ 0        (v ≠ w)
push(a)* · pop(a)* ≡ push(a)* + pop(a)*

StacKAT: infinite state network verificationPLDI'25

Deciding serializability

Deciding serializability in network systemsTACAS'26

2023

Feedback: you are crazy, GPT-4 can't even multiply 3-digit numbers.

They were right!

The argument I had

“Humans are incredibly stupid. Humans are even stupider than that at math.”

1. Humans are barely able to develop civilization.
2. Humans are very badly designed, given what physics allows.
3. Humans are not at all optimized for mathematics.
4. Mathematics is a game that is very well suited for a computer to play.
5. LLMs are impressively good at "pure intuition".

1. Humans are barely able to develop civilization

Not to scale

“Once civilization gets going, they fly to the moon in the blink of an eye.”

2. Humans are very badly designed

A whale brain is 6× larger.

Transistors switch a million times faster than neurons.

Nerve signals travel at about 100 m/s. Signals in a wire travel at about 200,000,000 m/s.

The laws of physics allow a lot more.

3. Humans are not at all optimized for mathematics

Selection pressure for mathematical ability has been very low.

We can do mathematics only because abilities such as pattern recognition also help us survive.

If mathematics had been useful for survival, we would be much better at it, with the same brains.

4. Mathematics suits computers

In chess, the gap between a grandmaster and a computer is enormous.

Mathematics is also a game with well-defined rules. Rocq and Lean show that it is a search problem.

In principle, brute force search proves every provable theorem. It just takes a long time.

5. LLMs are good at "pure intuition"

GPT-4 is better than humans at natural language, just by predicting the next word.

It can't do mathematics yet: it was not trained for it the way AlphaZero was trained for chess.

LLMs don't need to be very smart: just a good enough heuristic to cut the branching factor of proof search.

Why I didn't act on my own argument

• Most colleagues were skeptical.
• Does rational argument even work? It is just a string of words.
• Papers and careers require conventional work.
• Even believing it, I did not think enough about what to do differently, and it is hard.
• The research I was already doing was fun!

Bear with me: let's pretend arguments work.

What comes next?

• Mathematics: fully superhuman provers.
• Software engineering: autonomously build the entire software stack.
• Robotics: LLMs do better than robotics models (RoboHarm, 2026).
• AI development itself
• Biology: English description → DNA → pet?