是否可以在本仓库添加 Aya 开发组的宣传

[ice1000]

这是一个 proposal，请求单独提交一个介绍性的 section（以 issue 的形式或者仓库里的文件的形式都可以，本 issue 可能本身就构成一个广告），包含 Aya 编程语言开发组的一些广告。我目前的想法有这些：

• 首先，小组的初始的名字『类型小队』我感觉不够契合公司的二次元浓度。我结合《中二病也要谈恋爱》中的社团名字、编程语言的名字来源（妖怪之山鸦天狗记者——射命丸·搞个大新·文）的一社，以及 PLCT = 常盘台中学的设定，想到了两个名字『极东天狗昼寝结社』和『文文新闻报社』（下文将以『文文新闻报社』称呼 Aya 编程语言的开发组），设定为 PLCT 中学的一个社团。不知道这样的命名在宣传上会不会有更好的效果，以及是否符合公司的规范。
• Aya 这个项目源自于我的一条朋友圈和 @lazyparser 老板的一条评论，初始的动机其实是为了我自己和组员的学术生涯而开启的一个实验性项目。因为在我看来，近年编程语言的学术界的前沿研究已经达到了一个理论半饱和、需要和实践结合的状态（即，有很多存在于理论里的事物缺乏实际的实现）。其次，如果一个编程语言方面的工作仅存在于理论中，我们是很难发现它潜在的问题和全部的潜力的。如果我们能把一些功能实现出来，我们或许能发现更多的东西。我将在广告中讨论与此相关的思考。
  • 第一，实现出一个特性并且自己去用它写代码，我们才能对这个东西『有冇用』建立直观感受。
  • 第二，我们可能会在论文中犯错。实现是很好的测试手段。
  • 第三，实现编程语言本身就是一件很浪漫的事情。我希望在我死之前能创造一些美好的事物，也希望把拥有特殊才能的人利用起来。
  • 第四，我们有 @lazyparser 和 PLCT 的支持，所以我们也需要把 PL（编程语言理论）知识给 CT（编译器技术）化。
• 数量不菲的理论工作者并没有较好的编程基础和足够的软件工程功底（不是所有人都有魔理沙或者胡渊鸣那种理论实践双修的素质）来开发用户友好的学术研究型编程语言（看看 Agda 有多难安装，就可以知道）。我希望自己试一试，能不能在这方面做的更好。我挑战的目标是在用户体验上比肩甚至超过 Lean 和 Coq。我将讨论一些相关的思考。
• 文文新闻报社相对独立，因此和公司其他同学的交集不多，也缺少对外的 profile，只有一个空洞的 https://www.aya-prover.org 是不够的。我一直希望能把大家联系起来，但是我的组员好像都不怎么用微信。如果能在 GitHub 上引起大家的互动，那就太好了。
• 就像我在 PL talk 03 中提到的，编程语言和数学模型之间的关系可以产生很多有趣的研究，这是一个比较活跃的学术领域，有大量的工作可以做，而文文新闻报社就有进行这样的工作的后续计划。我不打算讨论这方面的计划，因为我要是全说了，遇到比我手快的人就会对我自己的学术生涯造成巨大的损失。Instead，我打算画一个不太清楚的饼（滑稽），因为我认为这样的工作对于想在未来跻身欧系编程语言理论研究的同学来说是很有魅力的，将这样的信息和资源广播出去总的来说是一件好事。
• 文文新闻报社的增员可能性。原则上我不想给老板添麻烦，而且更多的人不一定就会带来更高的效率，但是遇到真的优秀、也愿意来参与报社工作的同学（按照现在的分类标准，大概在 LV4 或者以上），我也想推荐到公司里，介绍大家认识啊。然而没有广告，哪来增员的可能性呢？所以我觉得我可能需要在一个和 PLCT 有关的地方放一些相关的文字来宣传我们的存在（这个仓库不得不说很厉害，连帝球都能吸引过来），并且简要描述报社需要具有哪些方面的才华的同学。为了避免喧宾夺主，我打算设立非常高的门槛。

[lazyparser]

当然欢迎啦～ 工作变多了可以招募更多的同学加入撒

[lazyparser]

weloveinterns 的仓库的目标：

1. 发布新的招聘信息。经常更新。
2. 展示实习生的成果。过去是经常把技术报告PR到这里，现在则更加倾向/鼓励实习生自己开GitHub/repo和zhihu/bilibili专栏，通过《PLCT开源进展》来index和引流。依然是作为孵化项目的地点的，不管是index还是直接把内容PR进来。
3. 作为实习生未来工作等活动的 能力和经历背书

[lazyparser]

可以直接把『极东天狗昼寝结社』或『文文新闻报社』的内容，或独立md文件或直接更新到README都可以。

[ice1000]

我觉得我应该严格限制一下……要么是利益相关（从事相关科研工作），要么是对设计或者实现顶级类型系统感兴趣的，不然就不招了 哈哈