Are we really gonna call this language "Don't know" in Cantonese?

[ice1000]

There are many alternatives that are both birds and are Chinese.

Essentially I want a name that fits the tradition (of using birds to name proof assistants, such as Coq, Agda, Arend, and let's kick Lean outside of this community) and is Chinese, but "mzi" might be too simple and hard to pronounce and is duplicate of Agda (though Agda is the name of a hen and mzi = hen, so to some extent Agda \in mzi, but the idea is still too similar, once we decide on a logo we'll have to realize this shameful similarity to the open public. However, using names from Chinese mythology is also somehow duplicate of a certain company's naming convention. It is then better to have a more modern Chinese name, to be distinct from all of these existing stuffs. I would propose Reiuji Utsuho or Okuu (おくう) which is the name of my favorite character in touhou (and the name instantly indicates a very good logo, and also make our proof assistant a touhou doujin), but that's Japanese and I'm just not sure. Maybe I should just use Okuu instead?

Since the codebase is not yet grown, rename a package won't be very fatal.

Let's think about this together.

[ice1000]

The logo instantly indicated by okuu, is not unique. There are many. Like the eye, the artificial sun, her spell cards, and these.

too large, click to expand

    credits (can't recall the exact order, but they're all listed): + https://www.deviantart.com/hellangelz/art/Utsuho-Reiuji-logo-155171802 + https://www.deviantart.com/greatpaperwolf/art/Flags-of-Touhou-Utsuho-Reiuji-364618599 + https://www.etsy.com/listing/479406147/touhou-project-reiuji-utsuho-okuu + https://www.reddit.com/r/touhou/comments/jafhpc/i_drew_utsuho_reiuji_with_powerpoint_as_always/?utm_source=share&utm_medium=web2x&context=3

A logo should be symbolic, but we can still use the ideas from these nice pics.

[imkiva]

Personally I like the Okuu name but I don't like the the last logo (radiation flag gives people a sense that they should keep it away from themselves). And I think the third one is better.

（Opening wings are really really my XP

[ice1000]

I second the remark on radiation flag. So, how do we choose between a concentric circle/oval one and ⑥ and others?

P.S. If we use ⑥, then our logo will be supported by standard unicode.

[ice1000]

Including opening wings will also be a good idea btw

[ice1000]

Also found these illustrations

• https://www.reddit.com/r/touhou/comments/inci1c/utsuho_the_solar_raven/
• http://www.animalhi.com/Birds/wings/touhou_wings_mecha_reiuji_utsuho_1582x900_wallpaper_30663

Anyways, I think the other members should also participate this discussion. We don't need a logo right now, because that's not important comparing to the typechecker, but the name is, since it's in our package name

[re-xyr]

Name: I think we can also give the crow Tengu’s (Aya and Hatate) a thought, as i prefer them more for unknown reasons (My fav Touhou character is Hieda no Akyuu, btw). Logo: If we are to use Reiuji Utsuho, then Circled 6 would be a bit pointless I think, but I somehow like the idea of the radiation symbol (maybe we can alter it a bit so it doesn’t look so threatening).

[ice1000]

Maybe we can just use the mzi name and answer mzi to those who ask why we're using this package name. The name of the language can be decided later ofc.

Naming, is hard. It's one of the two hardest problems of software engineering according to @tonyxty

[tonyxty]

Maybe we can just use the mzi name and answer mzi to those who ask why we're using this package name. The name of the language can be decided later ofc.

Naming, is hard. It's one of the two hardest problems of software engineering according to @tonyxty

I'm not powerful and confident enough to make such assertions; Phil Karlton said it. (if you search this man's name, the google results will make you think this quote is his most significant contribution :D) Also there are all kinds of variants.

[tonyxty]

Name: I think we can also give the crow Tengu’s (Aya and Hatate) a thought, as i prefer them more for unknown reasons (My fav Touhou character is Hieda no Akyuu, btw). Logo: If we are to use Reiuji Utsuho, then Circled 6 would be a bit pointless I think, but I somehow like the idea of the radiation symbol (maybe we can alter it a bit so it doesn’t look so threatening).

Hatate is not a bird! Sorry, I was thinking of Momiji. Hatate is totally a bird! But I like Aya a lot for her BGM in th10 and her spell card (dying to 幻想风靡 is oddly satisfying).

[tonyxty]

But overall, my suggestion is to name things later. I think many big companies do this too: they have codenames for internal projects, e.g., Vista was codenamed Longhorn before its release. So we can have project "codename mzi" which sounds cool.

[ice1000]

Yeah. mzi.

[tonyxty]

It suddenly occurs to me that, there is a professor at Fudan who taught me set theory and some first-order logic (and essentially opens the gate to logic for me) who also happens to be a bird expert and knows a lot of Chinese traditional texts. (he works in the Philosophy Dept.) Perhaps I can ask for his advice?

[ice1000]

Surely, and please do so!

[ice1000]

After a month I have some new thoughts unrelated to TH, that is Falco. He's a character in attack on titan who inherits the power of Jaw Titan and is able to fly (in some latest episodes). I guess his name is after Falcon. Well, but I'm still very into the idea of using TH characters. Let's see

[re-xyr]

Well, but I'm still very into the idea of using TH characters.

Me too.

[ice1000]

After a month I have some new thoughts unrelated to TH, that is Falco. He's a character in attack on titan who inherits the power of Jaw Titan and is able to fly (in some latest episodes). I guess his name is after Falcon. Well, but I'm still very into the idea of using TH characters. Let's see

There is a side note: It may not be a very good idea to expose the fact that we are using a name from a not-very-serious (like anime, music, etc.) subculture. Take Agda, they consider the origin of the name an embarrassing and everyone wants to hide it. Falco is good on this, it can relate directly to Falcon, while like Okuu, Aya, etc. are directly related to TH (and indirectly to birds) and people may be like trying to find about a programming language and found (potentially a bit erotic) a bunch of anime girl pics.

[re-xyr]

After a month I have some new thoughts unrelated to TH, that is Falco. He's a character in attack on titan who inherits the power of Jaw Titan and is able to fly (in some latest episodes). I guess his name is after Falcon. Well, but I'm still very into the idea of using TH characters. Let's see

There is a side note: It may not be a very good idea to expose the fact that we are using a name from a not-very-serious (like anime, music, etc.) subculture. Take Agda, they consider the origin of the name an embarrassing and everyone wants to hide it. Falco is good on this, it can relate directly to Falcon, while like Okuu, Aya, etc. are directly related to TH (and indirectly to birds) and people may be like trying to find about a programming language and found (potentially a bit erotic) a bunch of anime girl pics.

If you search Aya in Google, you won't find Shameimaru Aya.

I found one good point in Wikipedia.

Aya (あや, アヤ) is a common female Japanese given name meaning "design", "colorful" or "beautiful". Aya is also in use in the Hebrew language and means "to fly swiftly" or "bird". Aya is also an Arabic feminine name written as آية meaning "wonderful", "amazing", "miracle" or "verse" (of a religious scripture such as the Quran or Bible). In Mongolian, similar to Turkish, it means "goodness", "music", and "melody". In Chemehuevi, Aya means "tortoise". In Baoule on the Ivory Coast, Aya is given to the female born on Friday. To the Yoruba people, mostly in Nigeria.

So this makes a good pun. We can, for example, announce that the name Aya comes from Hebrew. But in fact, weebs would realize that it comes from Touhou

[imkiva]

Aya (あや, アヤ) is a common female Japanese given name meaning "design", "colorful" or "beautiful". Aya is also in use in the Hebrew language and means "to fly swiftly" or "bird".

Maybe Aya is a good name

[imkiva]

After a month, I found that if you want to pronounce mzi while speaking, it requires a sudden stop (switching to the Cantonese dialect and then switching back), which makes speaking very funny 😆

[re-xyr]

For further reference,

• the wikitionary page of the Hebrew word Aya (איה)
• the hebrew wikipedia page of Aya
  • corresponding EN wikipedia page, Pernis (Bird)

So, Aya in Hebrew is the bird genus Pernis, which includes four species of honey buzzards(蜂鹰).

[ice1000]

xy tql, wtcl

[re-xyr]

Another concern is if we take Aya, people might not be able to find our language by the single keyword. They have to search for “Aya language” or something. Lean has the same problem. In contrast, Agda, Coq and Idris do not have the problem.

[re-xyr]

If we choose Aya, that will also suggest some icons, for example, crow (but Aya in Hebrew is a buzzard, so I'm not sure if this will cause confusion), newspaper, maple leaf, camera, and her hat.

[re-xyr]

I just drew this. If we are to choose Aya, then this could be one prototype of the logo. It has an A inside, and also resembles Aya's hat.

[anqurvanillapy]

Well, what about Gugu, as gugu bird.

[ice1000]

Well, what about Gugu, as gugu bird.

No.

[tonyxty]

In addition, "Aya" is also used to express exclamation in multiple languages, especially when a mistake is accidentally made. In this aspect, it is similar to "mzi" in spirit --- a joke on things that people often say when working with a proof assistant.

Well, what about Gugu, as gugu bird.

I suspect you do f_cking know that "gugu bird" means p_n_s in Southeast Asia slang (and features prominently in a famous scandal in NTU, as shown in this video).

[anqurvanillapy]

In addition, "Aya" is also used to express exclamation in multiple languages, especially when a mistake is accidentally made. In this aspect, it is similar to "mzi" in spirit --- a joke on things that people often say when working with a proof assistant.

Well, what about Gugu, as gugu bird.

I suspect you do f_cking know that "gugu bird" means p_n_s in Southeast Asia slang (and features prominently in a famous scandal in NTU, as shown in this video).

No. Just a straight shout out to 鸽 meme. That's surprising.

[tonyxty]

In addition, "Aya" is also used to express exclamation in multiple languages, especially when a mistake is accidentally made. In this aspect, it is similar to "mzi" in spirit --- a joke on things that people often say when working with a proof assistant.

Well, what about Gugu, as gugu bird.

I suspect you do f_cking know that "gugu bird" means p_n_s in Southeast Asia slang (and features prominently in a famous scandal in NTU, as shown in this video).

No. Just a straight shout out to 鸽 meme. That's surprising.

Sorry for the false accusation. But still, a very hard NO.

[ice1000]

very♂hard♂no

[tonyxty]

Put your hand over my soft gugu♂bird~

Promise me we'll never make this repo public, ok?

[ice1000]

Put your hand over my soft gugu♂bird~

Promise me we'll never make this repo public, ok?

Hopefully

[ice1000]

:tada::tada::tada::tada::tada: