Are you familiar with the idea that to prove a loop correct only takes two things:
A/ proving (o->o), that it makes progress with each iteration, and
B/ proving (->o), that it terminates?
If so, he's speaking a bunch of different alien languages, showing how the same basic pattern (prove something for an infinite number of things by looking at their structure and proving something for the finite number of ways each of those things can be put together) works in each of the alien languages.
Or at least that's what I got from the few of those languages which I speak — all the rest are, as they say, greek to me.