There are a couple of technical typos in the post, but overall I found this a very cool and engaging read. It also reaffirms my belief that I find Coq neither fun nor readable (unlike Befunge which I find fun but unreadable, or Java, which I find readable but unfun).
Congratulations, Bernardo!