At my university, all majors of computer science have to take a course in discrete math, which involves writing a couple different types of math proofs using proof by induction (including strong induction) and proof by contradiction. However, that was the only class I've ever taken where I've had to write proofs regularly.
Anyway, I think that, at a minimum, at least one class like that should be part of every CS major's education, if it isn't already. That way, proofs are less intimidating, and things like Coq and Isabelle/HOL are less intimidating.
I agree with you, but the ship has sailed to retroactively require all programmers to have such experience. Also, the typical introductory discrete math course likely doesn't require writing proofs in a language precise enough to be formalized. I would think that we need at least one more introductory course to logic (first order logic, Peano axioms) and an introductory course to type systems (structural induction, progress and preservation, etc).
We also learned some first order logic, enough to write the proofs in formal language, though we didn't learn anything about type systems.
You're probably right about the ship having sailed, though. It's probably harder to get people to learn new things when they haven't been in school for a long time.
Anyway, I think that, at a minimum, at least one class like that should be part of every CS major's education, if it isn't already. That way, proofs are less intimidating, and things like Coq and Isabelle/HOL are less intimidating.