3 ms·

What is it with proof assistant designers and terrible naming instincts? "Lean" as a name collides with all sorts of business/engineering productivity framework

by mjfl 3y 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.

deleted 3y ago
[deleted]
lakesare 3y ago
I love "Lean" actually, have you noticed ∃∀. Googling Lean concepts does primarily return the codeine syrup links though yes.
- lupire 3y ago
  N for Natural numbers.
hcta 3y ago
you say that like it is a bad thing. Sign me up for the plane of existence without management frameworks please.
nanolith 3y 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.
ahhfgshando6698 3y ago
[dead]
nequo 3y 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=32519426#Nom_commun_1 https://fr.wiktionary.org/w/index.php?title=coq&oldid=325194... [2] https://github.com/coq/coq/wiki/Alternative-names https://github.com/coq/coq/wiki/Alternative-names
deleted 3y ago
[deleted]

by mjfl 3y ago

deleted 3y ago

[deleted]

lakesare 3y ago

I love "Lean" actually, have you noticed ∃∀. Googling Lean concepts does primarily return the codeine syrup links though yes.

lupire 3y ago
N for Natural numbers.

hcta 3y ago

you say that like it is a bad thing. Sign me up for the plane of existence without management frameworks please.

nanolith 3y 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.

ahhfgshando6698 3y ago

[dead]

nequo 3y 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=32519426#Nom_commun_1 https://fr.wiktionary.org/w/index.php?title=coq&oldid=325194... [2] https://github.com/coq/coq/wiki/Alternative-names https://github.com/coq/coq/wiki/Alternative-names

deleted 3y ago

[deleted]