QED

Alexandre Borovik wijst op een leuk bewijs van de onbeslisbaarheid van het stopprobleem. Het bewijs door Geoffrey K. Pullum is geschreven in de vorm van een gedicht:

Scooping the Loop Snooper - an elementary proof of the undecidability of the halting problem
No program can say what another will do.
Now, I won’t just assert that, I’ll prove [...]