Dependent-typed languages offer robust invariant checking, but the extensive proof effort has limited their adoption. Historically, projects like se L4 required significantly more time and code for proofs than for implementation.

Attempts to automate proofs with SMT solvers, like in F*, have shown promise but can falter on complex cases, leading to long run times and a need for 'mysticism' to satisfy the solver. The irrelevance of proof details, once correctness is established, combined with the emergence of LLMs, presents a new avenue for significant proof automation.

LLMs may reduce the burden of 'proof engineering' and help avoid type checker blow-ups. This could make dependent-type systems far more practical. The author built a Zstandard decompressor in Lean to explore this, noting Zstandard's efficiency over older compression formats like gzip and bzip2, and detailing its advanced entropy encoding (FSE) which, unlike Huffman coding, can achieve fractional bit usage per symbol on average.