alt Hacker Newsformal correctness proof is ridiculously hard, like, insanely hard, have you ever tried writing one for any real algorithm (not a platonic ideal quicksort)?
formal correctness proof is ridiculously hard, like, insanely hard, have you ever tried writing one for any real algorithm (not a platonic ideal quicksort)?
I 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.