Spotted this little gem in a thread about programming languages and software engineering, on (where else?) Lambda the Ultimate:

John Reynolds told me that he once described a correctness proof for XORing together pointers in a doubly-linked list to someone. This person asked why he would ever want to prove such a disgustingly nasty hack correct, to which he replied that it was no longer a disgusting hack, because he had a clean proof of correctness for it.