I'm from MIT EECS too. Just to clarify for other people - we have a pool of "required courses", from which we only need to choose a few. So it's not like we must learn Coq.

OTOH, I've TAed an undergrad research class and it's mind boggling how many people are doing Coq-related research.