By the way, what's with all the hate on Ben Pierce? Take his Software Foundations book. It opened up Coq in a very practical way. No crazy typing rules or cate

By the way, what's with all the hate on Ben Pierce? Take his Software Foundations book. It opened up Coq in a very practical way. No crazy typing rules or category theory. Just straight programming and simple proofs. That's a world where previously the few who entered were sucked down a rabbit hole of theory, never to return again.