@nprofile1q... @nprofile1q... if we had plenty spare time (ho ho ho) we should rejig all of the tripos discrete math, semantics, compilers, computability, etc to be backed up with (one or more) coherent collections of prover defns - maybe allowing but *not requiring* the students to learn how to drive them. How much that would or should skew out informal teaching isn't clear to me.