蝉语 是一个开源程序语言设计团队。
主要项目 Cicada 是一个 Dependently Typed 程序语言（类似 Coq、Agda、Idris 和 Lean）， 可以用来辅助证明数学定理，并却作为形式化的数学基础。
想要设计一个实用的计算机辅助证明系统的同时，这个语言也是大家学习与尝试新想法的基础。
程序语言设计就像 Web App 的设计一样，也分为 前端 与 后端， 前端包括语法设计与类型系统设计，后端主要在于代码生成与编译器优化。 我们的工作偏重于程序语言设计的前端。
工作内容：
- 维护 Cicada 的代码。
- 由 TypeScript 实现，OOP 编程风格。
- 编写文档来介绍我们的语言，以普及 机器辅助证明 与 形式化数学基础 相关的知识。
- 当前的文档在：https://cicada-lang.org/docs
- 探索类型系统的功能与实现方式。
- 例如 Inductive datatype、递归函数、子类型关系等等。
- 我们读类型论相关的书籍与论文，然后以研讨会和博客的形式分享。
入职要求：
- 能读英文。
- 对 程序语言设计 与 类型系统设计 感兴趣。
说明：
- 目前 Cicada 的代码有 10000 行左右（包括 REPL，以及模块系统）。 良好的代码结构在于容易理解（因而容易修改）， 我们努力注意保持良好的代码结构， 但是代码中还是有很多有待改进的地方。 也许通过讲解与讨论实现方式， 我们能获得清晰的理解与更好的代码结构。