Hacker News Reader

I know negative comments are frowned upon here, but I can't help pointing out that there is no language to talk about yet. Following this link, one will discover many notes and thoughts written by somebody who seems enthusiastic, passionate, and a little naive in my opinion about dependent types and formal verification. I wish him luck and will be curious to see what may come from this, but the results are probably years from now.

View on HN

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.

Reply on news.ycombinator.com