From the article:

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.

[...]

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. Strictness means that arguments to functions are evaluated before the call happens, whereas in Haskell the evaluation of arguments is deferred until the value is actually required. So in Haskell it's free to write expensive expressions and pass them into functions, because they'll only actually be computed if they end up being used. But it also means that computation can happen in very surprising places in the program. This is a contentious topic but, while I appreciate the elegance of laziness, boy, it can make the performance of programs hard to reason about.

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. Unfortunately, Lean does not have any aspects of a linear type system that I'm aware of, so it does not help you in ensuring that there is only a single reference to a value. It's a bit of a sharp edge that a seemingly minor tweak to the code can completely crater its performance by holding on to a reference to a large array somewhere inconspicuous. But it does mean that if you are trying to optimise the performance of something, you have a lot more tools at your disposal.

[...]

Combining dependent types and LLMs is not a new idea, but not much has been done on applying the combination to quotidian software engineering. Lots more experience would be needed. Very strong types can amplify the scope of changes as they have to be propagated out through all the derived types. Perhaps the proof effort scales poorly in larger systems, such that even modern LLMs can't keep up. Lean is a high-level language, and that's not suited to everything. (My toy Zstandard decoder is 10× slower than zstd on the command line.) Still, proof automation is here now and we, practically speaking, have a new type of programming language available to us. That's exciting!