At OPLSS 14, Andrew Appel characterized programming in Coq as the world's best video game, I would have to say it's a close second.

I recall it was accessible if you had programmed in an ML, start here: https://softwarefoundations.cis.upenn.edu/