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?