Just how bad of an idea is it for someone who knows programming and wants to learn math to try to work through a mathematics textbook with proof exercises, say Rudin's Principles of Mathematical Analysis, by learning a formal proof system like Coq and using that to try to do the proof exercises?

I'm figuring, hey, no need to guess whether whatever I come up with is valid or not. Once I get it right, the proof assistant will confirm it's good. However, I have no idea how much work it'll be to get even much simpler proofs that what are expected of the textbook reader right, how much work it'll be to formalize the textbook proofs even if you do know what you're doing and whether there are areas of mathematics where you need an inordinate amount of extra work to get machine-checkable formal proofs going to begin with.