We have proof automation now

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

The problem has always been that with great type-system power comes great proof effort. I can certainly attest to entire days spent proving really quite simple things. Doing proofs is actually quite fun: it's challenging, interactive, and there's a clear goal. But gosh, does it take a lot of time, especially if, like me, you don't know what you're doing. There's also the periodic, galling experience, at the end of many hours of effort, where you realise that the goal that you're trying to prove is, in fact, false.

That overhead has made programming in dependently-typed languages extremely niche. It has also spurred people to try and automate it away. The attempt I'm passingly familiar with is F*, where the system tries to have an SMT solver automatically discharge the obligations. That certainly works for simple cases, but it's very easy to craft something that causes the SMT solver to go off into space and run for hours, leaving you wondering whether it's ever going to finish.

We now have LLMs which, combined with proof irrelevance, promise to be an extremely capable form of proof automation. With sufficient amounts of automation perhaps you don't need to worry about proof engineering nearly so much. You 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 more practical. I wanted to play around with this so built a Zstandard decompressor in Lean, mostly because I was also curious about Zstandard.

Zstandard seems like it's winning the competition to replace gzip as the canonical compression utility. It's another LZ77-style compressor, but it offers better entropy coding and a careful design that allows it to achieve very impressive decompression speeds.

The job of an entropy encoder is, given a set of symbols with non-uniform probabilities, to encode a sequence of those symbols using the fewest number of bits. Zstandard uses Huffman trees, but it also has a higher-compression entropy encoder called FSE. FSE is a state machine. There are more states than symbols, and each symbol gets a fraction of the states that mirrors its probability of occurrence in the stream.

The central trick is that, by giving multiple states to more common symbols, the encoder doesn't just pick a symbol: it also picks which of that symbol's states to land in, and that choice carries information forward to the next symbol. That's where the fractional bits of information go. But this entropy encoder is still just table based, and so it runs very quickly.

Lean

Let's talk about Lean! Above I said that it's a dependently-typed language, and that is a concept better articulated in examples than in a complicated definition. Lean is a purely functional language like Haskell, although it has a few properties that make it potentially a lot more convenient as a programming language. Firstly, Lean is strict, while Haskell is lazy.

Next, Lean has some nice helpings of sugar. Its monadic do notation contains for loops and return statements and break statements. If you want to program in an imperative style, you can do so pretty reasonably!

Lastly, Lean has an optimisation where it will make mutating updates to objects as long as their reference count is equal to one. So you can mutate an array in place as efficiently as in an imperative language, as long as you are careful not to have a reference to it someplace else.

I wrote an implementation of the FSE table construction algorithm from the RFC. The RFC contains “test vectors” for it: three sample outputs from given probabilities. Obviously those go into unit tests. But, in Lean, we can also prove universal properties of the function.

These are the subtle assumptions that an optimised decoding inner-loop requires, and things that can only ever be implicit or mere comments in weaker type systems. Proving strong statements like that is part of the 10× effort that the seL4 retrospective described, and a major barrier to the adoption of dependent types in regular software. Several LLMs can do it automatically now in about 20 minutes, and using only a fraction of a $20/month subscription quota. It'll probably be table-stakes next year. Combining dependent types and LLMs is not a new idea, but not much has been done on applying the combination to quotidian software engineering. Still, proof automation is here now and we, practically speaking, have a new type of programming language available to us. That's exciting!

Aside: verified assembly

AWS made LNSym: a semantics and simulator for AArch64. That's cool. Perhaps we could use it to show equivalence between an optimised assembly implementation of some functions, and their Lean counterparts, and then use the assembly code at run-time? Then we could let LLMs rip at optimisation and they couldn't introduce any functional bugs. Verified assembly is well-trodden in crypto implementations, but perhaps now it could be cheap?