4 ms·
> However, the complexity of the algorithms, and, in particular, the presence of various special cases in the code which occur with very low but non-zero probab
by amelius 1mo ago
> However, the complexity of the algorithms, and, in particular, the presence of various special cases in the code which occur with very low but non-zero probability make it impossible to rule out the possibility of bugs remaining in the program.
Sounds like perhaps a nice testcase for formalization + AI?
- teiferer 1mo agoIt's beyond me why such foundational libraries don't have formal correctness proofs attached these days.
- winwang 1mo 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 1mo 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 1mo 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.
- deleted 1mo ago[deleted]