Hacker News new | ask | show | jobs
by mjfl 1007 days ago
What is it with proof assistant designers and terrible naming instincts? "Lean" as a name collides with all sorts of business/engineering productivity frameworks "Lean software development", "lean business management", "running a lean startup". And of course Coq is phallic both in English and the original French. It must be the case that the people that design these things live in a separate plane of existence where these things don't bother them.
4 comments
nequo 1007 days ago
Yes, unfortunately, Lean is harder to search for than some other programming languages. Although it seems workable: both DuckDuckGo and Google return Lean-related top results for me for "lean induction" and "lean match expression," for example.

> And of course Coq is phallic both in English and the original French.

Is it phallic in French too? I am not a French speaker. According to the French Wiktionary, "coq" means rooster, male chicken, cooked rooster, male partridge, a self-important person, a rooster on top of a church bell tower, a loose coin, a tool used for ironing, a kind of fish, a part used in watchmaking, or a cook working on a ship.[1] None of these sound phallic to me.

I have not seen evidence that this was intended as an English pun. Rather, it seems to have been a double pun in French, for the calculus of constructions (CoC) which Coq is based on, and Thierry Coquand who developed CoC.[2] So I just assume that it wasn't meant to be phallic and remind myself that some people speak French and they name their software French names.

[1] https://fr.wiktionary.org/w/index.php?title=coq&oldid=325194...

[2] https://github.com/coq/coq/wiki/Alternative-names

link
nanolith 1007 days ago
It's practically impossible to pick names that haven't been used for something else. I've taken to using the contraction of random amusing phrases when I want a unique name, but this isn't any better. Just fun (for me).

Relevant example: my current toy proof engine and language is called lesc. There are lots of things called "lesc", but none of them to my knowledge stand for Less Elegant Space Cowboy.

link
hcta 1007 days ago
you say that like it is a bad thing. Sign me up for the plane of existence without management frameworks please.
link
lakesare 1007 days ago
I love "Lean" actually, have you noticed ∃∀. Googling Lean concepts does primarily return the codeine syrup links though yes.
link
lupire 1007 days ago
N for Natural numbers.
link