It's a proof, but not a formal one. It doesn't define the notion of "program", for example. It's somewhere between an informal proof and a proof sketch (a correct and valid one, of course).
A formal proof is a sequence of statements where each is either an axiom or derived from previous ones via a set of derivation rules, and wherein assessing the validity of each axiom statement or derivation can be done "typographically" (mechanically and primitive-recursively). It's nigh-impossible to write a human-readable formal proof of anything interesting; the vast majority of mathematical papers published are informal proofs.
(Of course, this diversion doesn't detract from the matter of this proof-poem being very cool.)
Yes I am sorry, I believe I ment "it is in some ways a formal proof." It is indeed a proof sketch. With a preliminary section defining things more rigorously, I do believe that this is publishable in most of the Cryptography conferences I have published in.
Actually, that gives me a sort of unique idea: An online, wikipedia like proof database with understandable informal proofs with click-to-expand (inline) annotated sections, if you click them, they would expand into proof of less formal claims.
The idea would be that we generally share understanding of obvious axioms (and thus, allow them to be request-able assumptions), and so can enhance readability.
