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".