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.
