Re:The C standard formalized in Coq
by nickpsecurity on Monday November 30, 2015 @11:19AM
(#10650130)
Even the documentation mentions the issue and calls the name "unfortunate." So, it's a valid critique even if we should ignore it in discussions just to be productive. :)
[ Parent
| on HN ]
Really, where? I've always heard this was more intentional than unfortunate.
From the FAQ:
2 Did you really need to name it like that?
Some French computer scientists have a tradition of naming their software as animal species: Caml, Elan, Foc or Phox are examples of this tacit convention. In French, “coq” means rooster, and it sounds like the initials of the Calculus of Constructions CoC on which it is based.
Re:The C standard formalized in Coq
by nickpsecurity on Monday November 30, 2015 @01:36PM
(#10650893)
The name was intentional as they described. The common reception might have also been intentional as a joke of sorts. ;) Anyway, there was a page or interview where a rep called it "unfortunate" without going into detail. The implication in context was that the name's use in Britain or America often distracts from how the tool is used in a given paper. Hence, unfortunate choice of name.
Should've just picked a different animal haha. The name is easy to spell, though.
And also a tribute to Thierry Coquand, the inventor of the CoC.
Re:The C standard formalized in Coq
by nickpsecurity on Monday November 30, 2015 @03:45PM
(#10651603)
Yes, that was also in what I read.