4 ms·
It's beyond me why such foundational libraries don't have formal correctness proofs attached these days.
by teiferer 29d ago
It's beyond me why such foundational libraries don't have formal correctness proofs attached these days.
- winwang 29d agoimo, partially because it's still not easy (in terms of code -> formal proof). With AI, I've been Lean-ifying a simpler (but non-trivial) algo. Pointing (current) AI at it only goes so far and in fact might go "too far" in certain cases, where a non-formalized argument would have sufficed. There's also "who watches the watcher" -- did it really prove what we're supposed to prove? For something like these compression algos, though, I imagine it would be much easier since they already have actual proofs out there.
- mitxela 29d agoformal correctness proof is ridiculously hard, like, insanely hard, have you ever tried writing one for any real algorithm (not a platonic ideal quicksort)?
- teiferer 29d agoI have. And it is ridiculously hard. But having your decompression algorithm not produce what you compressed earlier is also ridiculously bad. So, seems worth the effort, given that AI can do lots the heavy lifting these days.