Bob Atkey's build systems are proof systems vs. Steve Loughran's build systems are not really just proof systems. (not really their titles, I am just paraphrasing for emphasis)
Matt Might's Yacc is dead vs. Russ Cox's yacc is not dead. There is a video of Matt Might talking about the 'Yacc is dead' work, which turned into a 2011 icfp functional pearl. I find it interesting how, very broadly speaking, their notion of "derivative of a parser" feels like a kind of "categorification" of the usual notion of derivative of a regular language. I couldn't tell you off the top of my head whether there are literally categories involved in any natural way, but it's a matter of equipping a thing with a extra data that feels very much like how morphisms capture the "how" of on object being related to another in multiple ways. (i.e. regular grammar just tells you whether you parsed or not, a parser gives you some data that is the parse tree)
