[wassenaar10]

Definitely a case to be made for that. The one time in undergrad where coq came up in a programming languages lecture, I distinctly remember thinking "haha penis".

[remexre]

We had a joke that our PL course is a maturity test, because Coq and Hoare triples come up in the same lecture...