ImperialViolet - We have proof automation now

ImperialViolet

We have proof automation now (26 Jul 2026)

I've long had a soft spot for dependently-typed languages like Coq Rocq and Lean.<br>They offer the possibility of a type system capable of encoding and enforcing<br>arbitrarily subtle invariants. The sort of thing that, in regular languages, ends<br>up (at best) as a comment, and which quickly gets lost as the size of the team grows.<br>Then you get subtle misunderstandings and components that don't quite<br>fit together. It's often the case that those components have grown to a<br>sufficient size that, when the problem is noticed, aligning either of them is a wearying prospect. Perhaps, say<br>dependent types seductively, you could write those invariants formally and have<br>a machine check them.

(p.s. Coq changed its name! I remember many years ago at a Coq conference in<br>Princeton, I tried suggesting that,<br>in an English-speaking world, having a programming language called Coq was an<br>impediment. I don't think the audience agreed at the time. I also joked that many of the talks there sounded like a speech by<br>Tyrion Lannister, there being so many Coqs and Hoares. A joke<br>that was hilarious and timely, even though it fell completely flat, coming as<br>it did before the final season of that show and our collective memory-holing of<br>it.)

The problem has always been that with great type-system power comes great<br>proof effort. I can certainly attest to entire days spent proving<br>really quite simple things. Doing proofs is actually quite fun: it's<br>challenging, interactive, and there's a clear goal. But gosh, does it take a lot<br>of time, especially if, like me, you don't know what you're doing. There's also the<br>periodic, galling experience, at the end of many hours of effort, where you realise that the goal<br>that you're trying to prove is, in fact, false. The classic result here is the<br>retrospective from the seL4 effort that found that, even though the project was<br>large enough for the engineers to develop considerable experience, they<br>spent about 10 times as much time proving as they did designing and<br>implementing. They ended up with more than 20 times as many lines of proof code as they<br>did C code.

That overhead has made programming in dependently-typed languages extremely niche. It has also spurred people to try and automate<br>it away. The attempt I'm passingly familiar with is F*, where the<br>system tries to have an SMT solver automatically discharge the obligations.<br>That certainly works for simple cases, but it's very easy to craft something<br>that causes the SMT solver to go off into space and run for hours, leaving you<br>wondering whether it's ever going to finish. I've seen that people who use<br>these languages a lot have to develop a sixth sense for what is going to make<br>the solver happy, and then craft everything around that. It can help,<br>but to an extent it converts the problem into mysticism: you end up<br>serving a complex and fickle god.

A critical fact is that, at least in theory, once the statement is correct, the contents of its proof<br>are irrelevant: only its existence matters. This is not entirely true<br>because of two complicating factors: first, what the seL4 group called &ldquo;proof<br>engineering&rdquo;: the need to structure proofs so that the effort of realigning them<br>after code changes is reduced. And, second, sufficiently complicated<br>proofs can cause even type checkers to blow up and consume vast amounts of<br>memory.

We now have LLMs which, combined with proof irrelevance, promise to be<br>an extremely capable form of proof automation. With sufficient amounts of<br>automation perhaps you don't need to worry about proof engineering nearly so much. You<br>still need to avoid blowing up the type checker but, in my limited tests, LLMs can avoid that. Potentially, LLMs suddenly make dependent-type systems dramatically<br>more practical. I wanted to play around with this so built a Zstandard decompressor<br>in Lean, mostly because I was also curious about Zstandard.

Zstandard seems like it's winning the competition to replace gzip as the<br>canonical compression utility. It's another LZ77-style compressor, but it offers<br>better entropy coding and a careful design that allows it to achieve very<br>impressive decompression speeds. It will never be as beautiful as bzip2, but<br>the shining elegance of the Burrows–Wheeler transform doesn't count for too<br>much in the face of significant practical advantages:

zstd

bzip2

gzip

lzma (XZ/LZMA2)

50<br>100<br>200<br>500<br>1000<br>2000<br>zstd<br>bzip2<br>gzip<br>lzma (XZ/LZMA2)

70<br>72<br>74<br>76<br>78<br>80<br>82<br>84<br>86<br>Compression tradeoff on 64 MiB of Lean/mathlib source<br>Space saved (%) — farther right is more compression<br>Decompression throughput (MiB/s, log scale) — higher is faster

(Measurements taken on the standard reference computer, i.e. whatever the author was using at the time. And note the log scale on the y-axis: gzip and Zstandard are in their own speed class. This is an Apple machine and Apple's gzip is especially optimised; expect gzip to...