[COURSE] Add Stanford CS242 (#493)

* add cs242

* 增加cs242英文，修改位置

* 删除了标题中多余的课程名称

* 修改英文版语病

docs/程序语言设计/CS242.en.md

@@ -0,0 +1,45 @@
+# CS242 Programming Languages
+
+## Descriptions
+
+- Offered by: Stanford
+- Prerequisites: basic knowledge about programming language theory and computer system
+- Programming Languages: OCaml, Rust
+- Difficulty: 🌟🌟🌟🌟
+- Class Hour: 60 hours
+
+CS242 is a course about programming languages (PL), but it is not a pure theoretical course in the traditional sense. This course first introduces classic PL theories such as Lambda calculus and type system, then uses the ideas and actual programming languages of system programming to motivate students to understand these theories, and shows how they help developers avoid various errors in actual programming.
+
+The instructor Will Crichton also wrote his course design ideas into a paper [From Theory to Systems: A Grounded Approach to Programming Language Education](https://arxiv.org/abs/1904.06750), which elaborates this teaching route from theory to systems.
+
+We help readers understand the specific content of this course by simply introducing each assignment:
+
+- Formalization and proof of JSON
+- Classic Lambda calculus in PL
+- Introduction to functional programming using OCaml
+- Use OCaml to implement a type checker and interpreter for a functional language, which is also a classic assignment in PL
+- Theory and practice of WebAssembly
+- Linear Type and Rust's ownership mechanism
+- Rust's asynchronous programming basics
+- Design state machines and implement session-typed TCP libraries using Rust's type system
+- The final assignment has four options:
+    1. Theorem proving in Lean
+    2. Read-Log-Update in Rust
+    3. Verified filesystems in F-Star
+    4. Deep learning framework in OCaml from a PL perspective
+
+These assignments cover a wide range of knowledge, from the classic PL theory and practice to the impact of programming languages such as Rust on programming and system design, and finally the distinctive projects. Almost all programming assignments have detailed local tests, especially the deep learning framework in the final project has more than 200 tests, which is suitable for self-study.
+
+The first few assignments are more about PL theory, and the later assignments are more about system programming.
+If you think that the course content and assignments in the first few times are too theoretical, you can focus on the assignment of implementing the interpreter using OCaml, which can not only help you have a deeper understanding of the previous theory, but also let you practice the type checking and interpretation of a functional language.
+
+The later assignments tend to use theory to guide system programming and design, especially Rust and its unique ownership mechanism and type system. Although we often have to fight with the compiler, this also just shows the significance of type systems and theories for programming and design.
+
+I personally feel that the assignments are difficult, but the gains are great. When the programming practice in the later assignments intersects with the theoretical knowledge learned before, there will be a pleasant feeling of sudden enlightenment. If you encounter difficulties in completing the assignments, this is normal. Please calm down and think carefully, or read the assignment guide again.
+
+## Course Resources
+
+- Course Website: [https://stanford-cs242.github.io/f19/](https://stanford-cs242.github.io/f19/)
+- Recordings: None, the main learning resources are the course notes and assignments
+- Textbooks: The first half of the course is based on the famous [TAPL](https://www.cis.upenn.edu/~bcpierce/tapl/), and the second half has no fixed textbook
+- Assignments: [Assignment Guide](https://stanford-cs242.github.io/f19/assignments/) and [Assignment Repository](https://github.com/stanford-cs242/f19-assignments)

docs/程序语言设计/CS242.md

@@ -0,0 +1,45 @@
+# CS242 Programming Languages
+
+## 课程简介
+
+- 所属大学：Stanford
+- 先修要求：对计算机系统和编程语言理论有初步了解
+- 编程语言：OCaml, Rust
+- 课程难度：🌟🌟🌟🌟
+- 预计学时：60 小时
+
+CS242是一门讲程序语言 (Programming Language, PL) 的课程，但不是传统意义上的纯理论导向。这门课程首先介绍了如 Lambda 演算，类型系统这样的经典 PL 理论，然后借助系统编程的思想和实际的编程语言来驱动学生理解这些理论，展示了它们是如何在实际编程中帮助开发者避免各种错误。
+
+主讲老师 Will Crichton 还将他的课程设计思想写成了论文 [From Theory to Systems: A Grounded Approach to Programming Language Education](https://arxiv.org/abs/1904.06750)，阐述了这条从理论走向系统的教学路线。
+
+我们通过简单介绍每个作业来帮助读者了解这门课程的具体内容：
+
+- 对 JSON 的形式化与证明
+- PL 中经典的 Lambda 演算
+- 以 OCaml 为例的函数式编程入门
+- 使用 OCaml 实现一个函数式语言的类型检查器和解释器，同样是 PL 的经典作业
+- WebAssembly 的理论与实践
+- Linear Type 和 Rust 的所有权机制
+- Rust 的异步编程基础
+- 利用 Rust 类型系统设计状态机和实现 session-typed TCP 库
+- 最后的大作业有四个可选项：
+    1. 使用 Lean 进行定理证明
+    2. 使用 Rust 实现 Read-Log-Update 同步机制
+    3. 利用 F* 语言验证文件系统的正确性
+    4. 在程序语言视角下使用 OCaml 实现一个深度学习框架
+
+这些作业涵盖知识跨度非常大，从最经典的编程语言理论证明和实践到以 Rust 为例的编程语言对于编程和系统设计的影响，再到最后各有特色的大作业。几乎所有的编程作业都有详尽的本地测试，尤其是大作业中的深度学习框架更有超过 200 个测试，适合自学。
+
+前面几次的作业偏 PL 理论，后面几次的作业偏系统编程。
+如果你觉得前面几次的课程内容和作业过于理论，可以重点尝试使用 OCaml 实现解释器的作业，它既能让你对之前的理论有更深刻的理解，又能让你实战一个函数式语言的类型检查和解释。
+
+而后面的作业则更倾向于利用理论来指导系统编程与设计，尤其是 Rust 和它独特的所有权机制与类型系统。虽然我们要经常与编译器搏斗，但这也恰好说明了类型系统和理论对于编程和设计的意义。
+
+个人自学过程中感觉作业还是偏难的，但收获很大，在后续作业的编程实践和前面所学的理论知识产生交集时会有恍然大悟的愉悦。如果你在完成作业时遇到了困难，这是十分正常的，请静下心来认真思考，或者再读一遍实验指导。
+
+## 课程资源
+
+- 课程网站：[官网](https://stanford-cs242.github.io/f19/)
+- 课程视频：无，主要学习途径是课程笔记和完成作业
+- 课程教材：前半部分是著名的[TAPL](https://www.cis.upenn.edu/~bcpierce/tapl/)，后半部分则无固定教材
+- 课程作业：[实验指导](https://stanford-cs242.github.io/f19/assignments/)与[作业仓库](https://github.com/stanford-cs242/f19-assignments)

mkdocs.yml

@@ -96,6 +96,7 @@ plugins:
           计算机网络: Computer Networking
           数据库系统: Database Systems
           编译原理: Compilers
+          程序语言设计: Programming Language
           计算机图形学: Computer Graphics
           Web开发: Web Development
           数据科学: Data Science
@@ -207,6 +208,8 @@ nav:
       - "CMU 15-799: Special Topics in Database Systems": "数据库系统/15799.md"
   - 编译原理:
       - "Stanford CS143: Compilers": "编译原理/CS143.md"
+  - 程序语言设计:
+      - "Stanford CS242: Programming Languages": "程序语言设计/CS242.md"
   - 计算机图形学:
       - "GAMES101": "计算机图形学/GAMES101.md"
       - "GAMES202": "计算机图形学/GAMES202.md"