One personal project I'd love to find the time for is to try to write out a sequence of math notes that essentially builds up a Lean repository, intentionally "refactoring" as it goes along. So you do some explicit coordinate vector or system-of-equation calculations with both real and complex numbers, eventually define interfaces for fields and vectors, do your linear algebra proofs, realize that linear endomorphisms are almost-but-not-quite a field, so define rings and go back and refactor your field proofs to use them, realize vector spaces are "K[T] not-quite vector spaces", define modules, refactor your vector space code, etc.

This was kind of how math classes worked, but without that explicit phrasing. It would certainly make the analogy between the two activities more obvious. I also wonder whether people would have less trouble with quantifiers if they were phrased in programming terms: a proof of "forall x, p(x)" is a function x=>p(x), and a proof of "there exists x such that p(x)" is a pair (x, p(x)). e.g.

Continuity: (epsilon: R, h: epsilon>0, x_0: R) => (delta: R, h2: (x: R, h3: d(x,x_0) < delta) => d(f(x),f(x_0)) < epsilon)

Uniform continuity: (epsilon: R, h: epsilon>0) => (delta: R, h2: (x: R, x_0: R, h3: d(x,x_0) < delta => d(f(x),f(x_0)) < epsilon))

proof of UC => C = (epsilon, h, x_0) => let delta, h2 = UC(epsilon,h) in (delta, h2(_,x_0,_))

So when you're trying to figure out how to do the proof, it's clear what kind of type you need to return and your IDE could help you with autocomplete based on type inference.