Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[COURSE] Add Stanford CS242 #493

Merged
merged 4 commits into from
Aug 17, 2023
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
增加cs242英文,修改位置
  • Loading branch information
Qi-Zhan committed Aug 17, 2023
commit 494429b0d4f4bc564730730c3a2738ace0ced00e
45 changes: 45 additions & 0 deletions docs/程序语言设计/CS242.en.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
# CS242 Programming Languages

## Descriptions

- Offered by: Stanford
- Prerequisites: basic knowledge about programming language theory computer system
PKUFlyingPig marked this conversation as resolved.
Show resolved Hide resolved
- 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, and 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 theoretical proof 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 assignment has more than 200 tests, which is suitable for self-study.

The first few assignments are more PL theory, and the later assignments are more 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 still 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/)
- 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)
5 changes: 3 additions & 2 deletions docs/程序语言设计/CS242.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
- 先修要求:对计算机系统和编程语言理论有初步了解
- 编程语言:OCaml, Rust
- 课程难度:🌟🌟🌟🌟
- 预计学时:60小时
- 预计学时:60 小时

CS242是一门讲程序语言 (Programming Language, PL) 的课程,但不是传统意义上的纯理论导向。这门课程首先介绍了如 Lambda 演算,类型系统这样的经典 PL 理论,然后借助系统编程的思想和实际的编程语言来驱动学生理解这些理论,展示了它们是如何在实际编程中帮助开发者避免各种错误。

Expand All @@ -28,10 +28,11 @@ CS242是一门讲程序语言 (Programming Language, PL) 的课程,但不是
3. 利用 F* 语言验证文件系统的正确性
4. 在程序语言视角下使用 OCaml 实现一个深度学习框架

这些作业涵盖知识跨度非常大,从最经典的编程语言理论证明和实践到以 Rust 为例的编程语言对于编程和系统设计的影响,再到最后各有特色的大作业。几乎所有的编程作业都有详尽的本地测试,尤其是大作业中的深度学习框架更有超过200个测试,适合自学。
这些作业涵盖知识跨度非常大,从最经典的编程语言理论证明和实践到以 Rust 为例的编程语言对于编程和系统设计的影响,再到最后各有特色的大作业。几乎所有的编程作业都有详尽的本地测试,尤其是大作业中的深度学习框架更有超过 200 个测试,适合自学。

前面几次的作业偏 PL 理论,后面几次的作业偏系统编程。
如果你觉得前面几次的课程内容和作业过于理论,可以重点尝试使用 OCaml 实现解释器的作业,它既能让你对之前的理论有更深刻的理解,又能让你实战一个函数式语言的类型检查和解释。

而后面的作业则更倾向于利用理论来指导系统编程与设计,尤其是 Rust 和它独特的所有权机制与类型系统。虽然我们要经常与编译器搏斗,但这也恰好说明了类型系统和理论对于编程和设计的意义。

个人自学过程中感觉作业还是偏难的,但收获很大,在后续作业的编程实践和前面所学的理论知识产生交集时会有恍然大悟的愉悦。如果你在完成作业时遇到了困难,这是十分正常的,请静下心来认真思考,或者再读一遍实验指导。
Expand Down
6 changes: 3 additions & 3 deletions mkdocs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,7 @@ plugins:
计算机网络: Computer Networking
数据库系统: Database Systems
编译原理: Compilers
程序语言设计: Programming Language
计算机图形学: Computer Graphics
Web开发: Web Development
数据科学: Data Science
Expand All @@ -104,7 +105,6 @@ plugins:
机器学习系统: Machine Learning Systems
深度学习: Deep Learning
机器学习进阶: Advanced Machine Learning
程序语言设计: Programming Language
后记: Postscript
- search:
lang: ja
Expand Down Expand Up @@ -208,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"
Expand Down Expand Up @@ -246,6 +248,4 @@ nav:
- "Columbia STAT 8201: Deep Generative Models": "机器学习进阶/STAT8201.md"
- "U Toronto STA 4273 Winter 2021: Minimizing Expectations": "机器学习进阶/STA4273.md"
- "Stanford STATS214 / CS229M: Machine Learning Theory": "机器学习进阶/CS229M.md"
- 程序语言设计:
- "Stanford CS242: Programming Languages": "程序语言设计/CS242.md"
- 后记: "后记.md"