IIRC Dijkstra advocated constructing a proof of your program first. This also involves debugging, mistakes and trial-and-error, just at a different level. Mathematical representations and proofs are powerful because general and certain; but they aren't magic and don't write themselves.
It's a lot easier - and a lot more fun - to deal with specific instances, that are concrete, and can be examined and experimented with on a computer.
Logically, one could also work with proofs with a computer to give the same benefits (e.g. coq proof assistant), but for some reason, it doesn't seem to be as much fun in practice. Perhaps because the abstract versions don't have a direct impact; they aren't "live" (idk).
Yup and I had to take two modules on it for my degree. I've never encountered anything so dull in my life! [That was probably because the material was presented in such a dry way, I'm pretty sure anything can be interesting if someone with passion is also a skilled presenter]
It's definitely the presentation. I also studied formal verification in my second year and used it as an opportunity to catch up on missed sleep.
However, the third year I studied how to formally define programming languages and really enjoyed it. It was all about delivery.
I think class size has an effect too - it's much easier to engage with smaller classes. The second year module was mandatory, whereas the third year module was optional.
It's a lot easier - and a lot more fun - to deal with specific instances, that are concrete, and can be examined and experimented with on a computer.
Logically, one could also work with proofs with a computer to give the same benefits (e.g. coq proof assistant), but for some reason, it doesn't seem to be as much fun in practice. Perhaps because the abstract versions don't have a direct impact; they aren't "live" (idk).