lean-zip beats every single compression level miniz_oxide provides, i.e. we're capable of providing the same compression at higher throughput. At its fastest setting we're 15% quicker and the output is 8.8% smaller.
However, the article also notes that while they managed to surpass Rust's miniz_oxide, they were no match for the end boss of DEFLATE performance: libdeflate, written in C.
lean-zip is certainly not the best here: libdeflate unsurprisingly blows it out of the water (unsurprisingly because this is a very carefully tuned implementation using architecture-specific SIMD, that we can't touch in Lean).
Enter Roc, a functional programming language (but not a theorem prover) with an explicit focus on runtime performance.
