We have proof automation now We have proof automation now (26 Jul 2026) I've long had a soft spot for dependently-typed languages like Coq Rocq and Lean. They offer the possibility of a type system c
By Coderz Club · 2026-07-27 · Tags: html
We have proof automation now
We have proof automation now (26 Jul 2026) 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. (p.s. Coq changed its name! I remember many years ago at a Coq conference in Princeton, I tried suggesting that, in an English-speaking world, having a programming language called Coq was an 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 Tyrion Lannister, there being so many Coqs and Hoares. A joke that was hilarious and timely, even though it fell completely flat, coming as it did before the final season of that show and our collective memory-holing of it.) 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. The classic result here is the retrospective from the seL4 effort that found that, even though the project was large enough for the engineers to develop considerable experience, they spent about 10 times as much time proving as they did designing and implementing. They ended up with more than 20 times as many lines of proof code as they did C code. 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. I've seen that people who use these languages a lot have to develop a sixth sense for what is going to make the solver happy, and then craft everything around that. It can help, but to an extent it converts the problem into mysticism: you end up 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 are irrelevant: only its existence matters. This is not entirely true because of two complicating factors: first, what the seL4 group called proof engineering : the need to structure proofs so that the effort of realigning them after code changes is reduced. And, second, sufficiently complicated proofs can cause even type checkers to blow up and consume vast amounts of memory. 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. It will never be as beautiful as bzip2, but the shining elegance of the Burrows–Wheeler transform doesn't count for too much in the face of significant practical advantages: (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 be slower elsewhere.) Zstandard (by Yann Collet, building on the seminal ANS work by Jarek Duda) has an RFC, but it is quite terse. It contains all the information you need to implement a decompressor, but unless you're already quite familiar with compression, I think you'll need to re-read it a few times to understand what's going on. I, at leas
We have proof automation now (26 Jul 2026) 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. (p.s. Coq changed its name! I remember many years ago at a Coq conference in Princeton, I tried suggesting that, in an English-speaking world, having a programming language called Coq was an 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 Tyrion Lannister, there being so many Coqs and Hoares. A joke that was hilarious and timely, even though it fell completely flat, coming as it did before the final season of that show and our collective memory-holing of it.) 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. The classic result here is the retrospective from the seL4 effort that found that, even though the project was large enough for the engineers to develop considerable experience, they spent about 10 times as much time proving as they did designing and implementing. They ended up with more than 20 times as many lines of proof code as they did C code. 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. I've seen that people who use these languages a lot have to develop a sixth sense for what is going to make the solver happy, and then craft everything around that. It can help, but to an extent it converts the problem into mysticism: you end up 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 are irrelevant: only its existence matters. This is not entirely true because of two complicating factors: first, what the seL4 group called proof engineering : the need to structure proofs so that the effort of realigning them after code changes is reduced. And, second, sufficiently complicated proofs can cause even type checkers to blow up and consume vast amounts of memory. 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. It will never be as beautiful as bzip2, but the shining elegance of the Burrows–Wheeler transform doesn't count for too much in the face of significant practical advantages: (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 be slower elsewhere.) Zstandard (by Yann Collet, building on the seminal ANS work by Jarek Duda) has an RFC, but it is quite terse. It contains all the information you need to implement a decompressor, but unless you're already quite familiar with compression, I think you'll need to re-read it a few times to understand what's going on. I, at leas