The boxer Mike Tyson put it well, "Everyone has a plan until they get punched in the mouth."

I discovered Coq and OCaml by way of the Frama-C framework for formally verifying C programs. This is a system that works today. It does need to be made lower friction to install and get started with, but the author of this repo bashes on Coq and its researchers as if he were a young firebrand politician taking on Big Tobacco and Big Pharma. He even says, 'And let's be honest, the name "Coq" is just terrible.'

I wish him well on his crusade against Big Coq.