These theorem proving projects which can't make a simple program like an analog clock, which is only 150 words of code, are depressing to me, showing how little progress has been made at improving programming. Lots of mathematical jargon like "cubical syntax"; near zero utility outside a mathematical conference.

i wish i could understand this stuff better—it seems like the universe/homotopy level might have connections to asai’s reflective language black scheme:

Self-modifying code produces the smallest, most powerful programs you can imagine, however it also has the worst scores for MTTR BSOTTA (mean time to repair by someone other than the author). LISP will always be a fascinating language for some, but be an anathema in commercial situations where maintenance dominates. However, if you are smart enough, you can pull it off, as Autocad was written in LISP originally, and that is one of the greatest programs ever written.