>>3
Coq (and HOL, and Z, and VDM) is great, I learned the basics myself. But that's more for personal interest, I think these techniques probably only make sense for 1-5% of software projects. That's what I meant by a "step back", I think a good static type system, e.g. *ML/Haskell, and contract-based development can get you 80% of the benefits but now your techniques are applicable to more than half of projects. And ML or Prolog is fairly widely taught around here, even though you could graduate with the impression that the toy subset you were taught is the whole language when actually they have everything needed to run industrial-strength projects.