I took that course as well, and for me, the big takeaway wasn't that I specifically want to use Coq for anything practical, but the idea that you can actually do quite a lot with a non-Turing complete language. Realizing that constraints in a language can be an asset rather than a limitation is something that I think isn't as widely understood as it should be.