A colleague just shared this gem with me:
Starting with two premises — that all software contains bugs and that all software can be built with fewer lines of code — one can inductively prove that all programs can be reduced to a single line of code that doesn’t work.