Also while the NeurIPS name thing is totally tangential to this entire fiasco, as someone whose life work is on a system named by some French dude in the 1980s as an intentional joke to make anglophones talk about men's genitals, I have so much respect for that name change.
Conversation
Even worse, the same joke was perpetuated in naming Agda, but with a strange allusion to Swedish folk music? Come on.
3
11
This is the namesake of Agda like you all had so many years to not perpetuate the genitals jokes and yet
4
11
Woah I had no idea how dirty this song was. The Wikipedia page makes it seem very tame… I *preferred* talking about Agda because it caused less questions. 😬
1
3
Advice from Coq devs is to use "Gallina" around total strangers if Coq raises too many questions
1
3
13
Thanks! I was confused by why both names were used in places, but this makes a ton more sense. To be honest I wish it was more explicitly said, but I understand the difficulty.
1
2
Officially, Gallina refers to the proof term language, but it serves this purpose well enough.
1
3
Replying to
Yeah was aware, more was confused when it was used to refer to the system itself. 😅