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

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/ https://softwarefoundations.cis.upenn.edu/