@nprofile1q... @nprofile1q... Marcelo and I keep talking about this... It's a very interesting idea. One challenge is to find a proof assistant that is viable for this kind of thing — meaning, one that is not too powerful (so that it obliterates the thing we are trying to teach), not too speculative in its design (so that one cannot conclude anything about mathematics from the fact that it is proved), not to crufty and difficult to use and/or install, etc.....

I might wish to revisit this question once my own proof assistant is up and running ;-)

In the meanwhile, I have been thinking a lot about how we might rejigger the course so that things are done in a way that is closer to the formal way, which usually is the easier way anyway. For example, discrete maths should probably be inverted so that functions and data types are primitive and relations are defined notions, and encodings of data types as big intersections is ...... simply deleted. etc.