Well, the title of this post pretty much tells the story; Geoffrey K. Pullum has published a proof that the Halting Problem is undecidable, in verse. Here’s an excerpt:
Here’s the trick that I’ll use – and it’s simple to do.
I’ll define a procedure, which I will call Q,
that will use P’s predictions of halting success
to stir up a terrible logical mess.
Do read the whole thing, as it actually does contain a peer-reviewed proof.
Personally, I find rhyme and meter to be underused tools in the fields of mathematics and computer science. I suspect that most programmers don’t read technical journals at all; making the research more entertaining can only help the field. Then again, I’ve been known to cancel spam in verse, so my opinion may be outside of the mainstream.
So anyway, I’m off to adapt Beowulf into a proof in epic verse of the Taniyama–Shimura conjecture. I’m still dithering over whether to base my adaptation on Seamus Heaney’s translation, or the original, Old English.