Regarding 1), I meant bizarre to non-mathematicians. Most people are familiar with arithmetic and perhaps even geometry proofs, but not so much with proofs that involve ordinals and multiple levels of infinity. That such a simple program requires more than (Peano) arithmetic to prove statements about its behavior seems very unintuitive, at least to me.

2) Yeah that’s actually how I discovered Goodstein sequences. I saw some post on HN about tiny Turing machines that halt iff ZFC is consistent and wanted to learn more.