I made a little progress on a very silly project: To rewrite the definitions in Quine's _Mathematical Logic_ as Elisp programs, and thereby, eventually, to write out "1+1=2" in his canonical language (nothing but "is a member of", "nor", and parentheses), which he says "would run to a length of many pages".