tbf the fact that there's ads on public transport is kinda dystopian enough in and of itself
do you think the version of coq a proof is written in is a good proxy for when the authors started writing the proof, or just a proxy for when they last bothered updating it?
like did that shit just happen automatically the day I started estrogen, and if so, how did they know?!