7 hours ago
- Dependently-typed languages like Lean offer powerful type systems but require significant proof effort, as seen in the seL4 project with 10x more proof code than implementation code.
- LLMs combined with proof irrelevance (the fact that only existence of proof matters) can automate proof generation, making dependent types more practical for everyday software engineering.
- Zstandard is a modern compression utility that uses Huffman and FSE (Finite State Entropy) coding; FSE achieves fractional bits per symbol by assigning multiple states to common symbols.
- Lean is a strict, purely functional language with mutation optimization (when reference count is 1) and support for imperative-style coding, making it suitable for performance-sensitive tasks.
- The author built a Zstandard decompressor in Lean and used LLMs to automatically prove properties of the FSE table construction, such as table size, state counts, and reachability of all states.