{"topic":{"id":9648,"title":"如何双修数学计算机","slug":"topic","categoryId":14,"createdAt":"2024-02-23 15:55:34.010385","bumpedAt":"2024-10-26 15:35:26.264029","views":423,"postsCount":6,"highestPostNumber":6,"likeCount":4,"closed":false,"pinned":false,"pinnedGlobally":false,"pinnedAt":null,"pinnedUntil":null,"isBanner":false,"excerpt":"很想双修数学和计算机，但是只对计算机的理论部分感兴趣（lamda 演算，类型论等），有什么课程推荐吗","deletedAt":null,"isAnonymous":false,"category":{"id":14,"name":"问答","slug":"qa","color":"f5c211"},"author":{"id":1047,"username":"anonymous_coward_old","name":"Anonymous Coward Old","avatarUrl":"/uploads/image/43/32/4332638c11248b8ff07033c11de0759a55205facfbec85e14458245a91991faf.avif"},"tags":[]},"posts":[{"id":24189,"postNumber":1,"raw":"很想双修数学和计算机，但是只对计算机的理论部分感兴趣（lamda 演算，类型论等），有什么课程推荐吗","cooked":"

很想双修数学和计算机，但是只对计算机的理论部分感兴趣（lamda 演算，类型论等），有什么课程推荐吗

\n","createdAt":"2024-02-23 15:55:34.0845","updatedAt":"2024-02-27 14:25:06.949279","replyToPostNumber":null,"replyCount":0,"likeCount":0,"wordCount":43,"liked":false,"bookmarked":false,"polls":[],"reactions":[],"wiki":false,"version":2,"publicVersion":2,"deletedAt":null,"isAnonymous":false,"user":{"id":1047,"username":"anonymous_coward_old","name":"Anonymous Coward Old","avatarUrl":"/uploads/image/43/32/4332638c11248b8ff07033c11de0759a55205facfbec85e14458245a91991faf.avif","admin":false,"moderator":false,"signatureRaw":null,"signatureCooked":null}},{"id":24218,"postNumber":2,"raw":"cy","cooked":"

\n","createdAt":"2024-02-24 03:52:06.646194","updatedAt":"2024-02-24 03:52:06.646194","replyToPostNumber":null,"replyCount":0,"likeCount":0,"wordCount":1,"liked":false,"bookmarked":false,"polls":[],"reactions":[],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"isAnonymous":false,"user":{"id":30,"username":"一只玉米人","name":"玉米🌽","avatarUrl":"/uploads/blob/14/96/14961aeaa46ccbb75a61eec0c27b26e74fb5d1c00ccdcbbe898ca9ea37087dd6.svg","admin":false,"moderator":true,"signatureRaw":"*年月擦身过，暂且问，会更好吗？*","signatureCooked":"

年月擦身过，暂且问，会更好吗？

\n"}},{"id":24232,"postNumber":3,"raw":"首先，计算机这个学科工程性还是挺强的。所以如果你只对可计算性理论和计算复杂度理论感兴趣，而对任何代码都完全不感冒，那么个人认为你实际上是对**某些数学分支**而不是“计算机的理论部分”感兴趣。作为一个数学水平不太好的计算机学生，我对这种情况实在是爱莫能助。\n\n反之如果你觉得 lambda 演算之类的东西比较有意思并且愿意在计算机上玩玩它，那么也许你可以尝试**函数式编程** (functional programming) 和**程序语言** (programming languages) 领域的知识，辅以关于**形式化方法**的内容。（以下推荐的课程部分来自 [CS 自学指南](https://csdiy.wiki)）\n\n- 函数式编程是一种与命令式编程（例如 C 语言）差异很大的编程范式，一般比较喜欢数学的朋友也都会比较喜欢函数式编程，并且学习函数式编程对学习程序语言和形式化都有帮助。因为我并不擅长此道，所以就不胡乱介绍了，可以选一门课：\n - [Haskell MOOC](https://csdiy.wiki/%E7%BC%96%E7%A8%8B%E5%85%A5%E9%97%A8/Haskell-MOOC/)，依托 Haskell 语言讲授\n - [Cornell CS3110](https://csdiy.wiki/%E7%BC%96%E7%A8%8B%E5%85%A5%E9%97%A8/CS3110/)，依托 OCaml 语言讲授\n- 程序语言（一般简称为 PL）是以设计和分析**编程语言**为目标的理论，实际上由若干不同的分支组成，其中就包括你提到的类型理论。由于涉及的东西多且研究人员较少，国内这方面的课程其实比较薄弱。可以看看 [Stanford CS242](https://csdiy.wiki/%E7%BC%96%E7%A8%8B%E8%AF%AD%E8%A8%80%E8%AE%BE%E8%AE%A1%E4%B8%8E%E5%88%86%E6%9E%90/CS242/) 这门课。这门课里也有 OCaml 函数式编程，或许不需要函数式编程课作为前置基础。\n- 形式化方法比较倾向于分析和验证**软件**的正确性，产生了一些互联网上不太出名但影响非常深远的软件系统，比如说 seL4 操作系统内核。可以看看科大黄文超老师开的 [形式化方法导引](https://faculty.ustc.edu.cn/huangwenchao/zh_CN/zdylm/680196/list/index.htm) 课程（没有视频但开放课件和参考资料），我看科大的同学对这门课评价相当不错。\n\n最后，顺便找到一篇看起来不错的知乎文章：[浅谈编程语言研究与程序分析](https://zhuanlan.zhihu.com/p/45208498) ，也许会有所帮助，祝好。","cooked":"

首先，计算机这个学科工程性还是挺强的。所以如果你只对可计算性理论和计算复杂度理论感兴趣，而对任何代码都完全不感冒，那么个人认为你实际上是对某些数学分支而不是“计算机的理论部分”感兴趣。作为一个数学水平不太好的计算机学生，我对这种情况实在是爱莫能助。

反之如果你觉得 lambda 演算之类的东西比较有意思并且愿意在计算机上玩玩它，那么也许你可以尝试函数式编程 (functional programming) 和程序语言 (programming languages) 领域的知识，辅以关于形式化方法的内容。（以下推荐的课程部分来自 CS 自学指南）

函数式编程是一种与命令式编程（例如 C 语言）差异很大的编程范式，一般比较喜欢数学的朋友也都会比较喜欢函数式编程，并且学习函数式编程对学习程序语言和形式化都有帮助。因为我并不擅长此道，所以就不胡乱介绍了，可以选一门课：\n
- Haskell MOOC，依托 Haskell 语言讲授
- Cornell CS3110，依托 OCaml 语言讲授
\n
程序语言（一般简称为 PL）是以设计和分析编程语言为目标的理论，实际上由若干不同的分支组成，其中就包括你提到的类型理论。由于涉及的东西多且研究人员较少，国内这方面的课程其实比较薄弱。可以看看 Stanford CS242 这门课。这门课里也有 OCaml 函数式编程，或许不需要函数式编程课作为前置基础。
形式化方法比较倾向于分析和验证软件的正确性，产生了一些互联网上不太出名但影响非常深远的软件系统，比如说 seL4 操作系统内核。可以看看科大黄文超老师开的形式化方法导引课程（没有视频但开放课件和参考资料），我看科大的同学对这门课评价相当不错。

最后，顺便找到一篇看起来不错的知乎文章：浅谈编程语言研究与程序分析，也许会有所帮助，祝好。

\n","createdAt":"2024-02-24 08:36:37.8521","updatedAt":"2024-02-24 08:36:37.8521","replyToPostNumber":null,"replyCount":0,"likeCount":2,"wordCount":650,"liked":false,"bookmarked":false,"polls":[],"reactions":[{"reaction":"❤️","count":2,"users":[{"id":1047,"username":"anonymous_coward_old","name":"Anonymous Coward Old"},{"id":6205,"username":"uika_winwing","name":null}],"hasReacted":false}],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"isAnonymous":false,"user":{"id":1381,"username":"greyishsong","name":"greyishsong","avatarUrl":"/uploads/image/da/bc/dabc731b0311f59850625bbeb55ed969fcfac0430c5ef0f68441e5466b7aa496.avif","admin":false,"moderator":true,"signatureRaw":null,"signatureCooked":null}},{"id":24233,"postNumber":4,"raw":"[quote=\"greyishsong, post:3, topic:9648, username:greyishsong\"]\r\n[浅谈编程语言研究与程序分析](https://zhuanlan.zhihu.com/p/45208498)\r\n[/quote]\r\n\r\n\r\n这篇文章作者是南大一位新来的老师。在 b 站有上传静态分析的课程。","cooked":"

\n\t\t\t\t\t\t\t

\n\t\t\t\t\t\t\t\t

\n\t\t\t\t\t\t\t\t\t

\n\t\t\t\t\t\t\t\t\t\t\n\t\t\t\t\t\t\t\t\t

\n\t\t\t\t\t\t\t\t\tgreyishsong:\n\t\t\t\t\t\t\t\t

\n\t\t\t\t\t\t\t\t

\n\t\t\t\t\t\t\t\t\t\n\t\t\t\t\t\t\t\t\t\n\t\t\t\t\t\t\t\t\t\t\n\t\t\t\t\t\t\t\t\t\n\t\t\t\t\t\t\t\t

\n\t\t\t\t\t\t\t

\n
浅谈编程语言研究与程序分析
\n

\n\t\t\t\t\t\t

这篇文章作者是南大一位新来的老师。在 b 站有上传静态分析的课程。

\n","createdAt":"2024-02-24 08:52:32.564515","updatedAt":"2024-02-24 08:52:32.564515","replyToPostNumber":null,"replyCount":0,"likeCount":0,"wordCount":51,"liked":false,"bookmarked":false,"polls":[],"reactions":[],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"isAnonymous":false,"user":{"id":1047,"username":"anonymous_coward_old","name":"Anonymous Coward Old","avatarUrl":"/uploads/image/43/32/4332638c11248b8ff07033c11de0759a55205facfbec85e14458245a91991faf.avif","admin":false,"moderator":false,"signatureRaw":null,"signatureCooked":null}},{"id":25380,"postNumber":5,"raw":"mit 双修 math eecs 不知道怎么做到的，也许全部翘课自学可以前两年学完你交开和不开的本科 5 个方向 math 课，后两年翘课自学 csdiy？\r\n这样可能不能毕业","cooked":"

mit 双修 math eecs 不知道怎么做到的，也许全部翘课自学可以前两年学完你交开和不开的本科 5 个方向 math 课，后两年翘课自学 csdiy？
\n这样可能不能毕业

\n","createdAt":"2024-03-02 10:38:30.023158","updatedAt":"2024-03-02 10:38:30.023158","replyToPostNumber":null,"replyCount":0,"likeCount":0,"wordCount":61,"liked":false,"bookmarked":false,"polls":[],"reactions":[],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"isAnonymous":false,"user":{"id":1047,"username":"anonymous_coward_old","name":"Anonymous Coward Old","avatarUrl":"/uploads/image/43/32/4332638c11248b8ff07033c11de0759a55205facfbec85e14458245a91991faf.avif","admin":false,"moderator":false,"signatureRaw":null,"signatureCooked":null}},{"id":42098,"postNumber":6,"raw":"Type Theory 是很小众的领域，其实在全球范围内研究的人也不多，所以视频课程相对少很多。想要入门可以先从学习简单的定理证明器（PA）开始，比如 Agda, Idris, Coq 还有现在很潮的 Lean4. \n对 PA 相对了解之后可以看一些类型论基础读物，推荐下面两本：\n- Type Theory and Formal Proof\n- Homotopy Type Theory\n\n在这之后可以找一些对口领域的论文读读。","cooked":"

Type Theory 是很小众的领域，其实在全球范围内研究的人也不多，所以视频课程相对少很多。想要入门可以先从学习简单的定理证明器（PA）开始，比如 Agda, Idris, Coq 还有现在很潮的 Lean4.
\n对 PA 相对了解之后可以看一些类型论基础读物，推荐下面两本：

Type Theory and Formal Proof
Homotopy Type Theory

在这之后可以找一些对口领域的论文读读。

\n","createdAt":"2024-10-26 15:35:26.264029","updatedAt":"2024-10-26 15:35:26.264029","replyToPostNumber":null,"replyCount":0,"likeCount":2,"wordCount":130,"liked":false,"bookmarked":false,"polls":[],"reactions":[{"reaction":"❤️","count":2,"users":[{"id":4668,"username":"IO","name":null},{"id":6205,"username":"uika_winwing","name":null}],"hasReacted":false}],"wiki":false,"version":1,"publicVersion":1,"deletedAt":null,"isAnonymous":false,"user":{"id":5150,"username":"CAIMEOX","name":"CAIMEO X","avatarUrl":"/uploads/image/ac/31/ac31a007f6ad9a4c78ae834f4e22eeef381832ee374f62037aac06d9a68ebf9a.avif","admin":false,"moderator":false,"signatureRaw":null,"signatureCooked":null}}],"hasMore":false,"lastReadPostNumber":1,"hasUrlPostNumber":false}