It seems like things after it (validity, soundess of
algorithmic equality) ought to be clear sailing, but
maybe I'm wrong about either that or the correctness
of my proof, or both.
Did some hacking on the TeX stuff for work.
K's off at an atypically Saturdayish Type-Thursday event, so I stuck around the apartment hiding from 100-degree heat, and noodled around with…
Playing around with the agda javascript backend, now. Like, my ears are popping from the sudden change of type-theory-pressure.
https://deadlockempire.github.io is a very cute edutainment game, meant to teach people about deadlocks and race conditions and concurrency…