#视频
科普视频，讲解了类型论的作用：《Why should you learn Type Theory?》

Reference：
* 类型系统推荐书籍

#项目
最近都在看类型系统的书籍TAPL，里面数学符号、公式很多，感觉Markdown在处理这种数学公式很多的笔记方面还是不够，于是开始用三脚猫的Latex来记一些笔记。

找到 李文威 老师开源的《代数学方法》项目中的一套Latex模板，感觉挺不错的，就照搬出来成了一个单独的项目，后续记Latex笔记都可以用得到：https://github.com/lichuang/latex-template 。另外《代数学方法》一书已经出版，所以老师开源的这套Latex代码，也可以作为学习Latex排版的一个不错的范例。

#生产力工具
之前好像并没有在电报频道里专门推荐过Relingo这款插件，今天专门写一下。

最开始了解到这个插件，是因为有网页生词提示、记忆的功能，感觉挺实用的，于是就第一时间买断了。

经过半年多的迭代，现在这个插件还能实时翻译youtube的字幕了，感觉这个功能也很实用。

除此以外在阅读英文网页的时候还可以翻译一段文字，外带提供的是DeepL翻译引擎的结果，光是DeepL的会员就值回票价了。

买得早所以当时100多就买断了，现在lifetime会员需要49刀的价格了。

#杂

出自微博：https://weibo.com/2167039312/N1lW7qoyE

#杂
北京时间2023年5月28日早上10:45分，国产大飞机C919商业首航。

Reference:
https://t.me/codedump_notes/420

#课程
继续我的类型系统（当前在阅读TAPL）自学之旅，找到几个以这本书为主要教材的课程及视频：

* 北大《编程语言的设计原理》：基本按照TAPL书上的内容来讲解的，可以认为划出了每章的重点。
* cornell的CS4110《Programming Languages and Logics》：有很多TAPL以外的内容，还讲了类型系统这部分内容的数理逻辑基础。
* cornell的CS6110《Advanced Programming Languages》：还没仔细看，不知道和CS4110有什么区别。
* 油管上的一个视频课程：内容挺好的，但是貌似没有继续更新了。

除此以外，暂时这类课程好像找不到其他视频类的教程了。

#人工智能
大概一个月以前看了一篇文字版本的陆奇对大模型的演讲，昨晚在B站闲逛找到了完整的视频，不过看起来视频和文章不是同一个演讲，但是总体来说看演讲视频效果还是能更好一些。

视频版：《陆奇最新演讲完整视频｜大模型带来的新范式》
文字版：《陆奇最新演讲实录：我的大模型世界观》

#项目推荐
crabviz：Rust写的基于LSP协议可以生成多种编程语言调用图关系的工具

https://user-images.githubusercontent.com/20551552/242812058-60584f59-a8f0-4a56-90eb-373c3f3b8cd5.gif

由于电报频道自带的搜索功能并不强大，所以我把数据同步导入了一份到：https://app.shokichan.com/c/tg/codedump_notes ，这里提供更强大的搜索功能。本频道的RSS订阅地址：https://rsshub.app/telegram/channel/codedump_notes

#高等教育
‘高等院校三千所’网页将以‘大规模集成网页(LSIP)’形式收录中国高校名单全集和网址，按照‘先中央后地方’、‘先本科后专科’的顺序形成中国高校层级图谱。针对普通高考录取，本页收录网址排除了成人高校，增补了港澳台高校，总院校链接数维持在三千左右。

#类型系统
《类型检查：时常被忽略的编译器组件》，个人觉得不错的一篇类型系统的科普文。

#文章
图灵奖得主 Richard W. Hamming《You and your research》的中文翻译稿

#数据库
慕尼黑工业大学数据库查询优化课程，搭配了600多页的 讲义。

#杂
高考可能是成年人面对的最后一个：有出题范围、有标准答案、限定时间内完成，又能给后续人生以极大影响的事情了。

从这个意义上来说，高考也难也不难，难的部分自不必说，不难是说高考的限制性很多、开放性很少。

等走向社会了，面对的很多都是开放的问题，而这些问题往往出题人是自己，做题人又是自己。比如XX的意义是什么，不同的人有不同的答案。其次没有了时间限制，答案会随着时间发生不同的变化。一个事情你20岁的时候也许做不到，努力到了30岁行不行？毕竟没有给你限制“答题”时间。这个问题反过来也是的，你20岁的时候能做到的事情，如果随着时间过去没有自己去对抗熵增，很可能过了几年能力就退化了。

很多人学生时代能考高分，出了社会不太行，我自己的观察就是不善于给自己出题，以前在学校都有明确的学习范围，出了社会得自己给自己找题目、找方向，他们也不善于回答没有标准答案的问题，习惯了被别人的标准答案（比如身边人、家里人、社会上）所裹挟。

总而言之吧，我读高中的时候老师经常给我们说：好好学习，等考上了大学随便你们玩，其实我即便到了高三还能经常下午放学了踢个一小时球，我怀念那种无忧无虑只为了一个有各种限定的答卷而努力的日子，这样的日子于我而言大概是不会再有了。

回到最开始的讨论，既然以后的日子可以自己出题自己解题，那么就连“高考能不能一考定终身”这个问题都值得去定义和解决了。

#Rust
早年学C++的时候，觉得如果只推荐一本C++的书，那一定是《Effective C++》，这本书总结了C++里最重要、常见的一些知识点，事实上我甚至认为任何领域都需要这样一本总结出最常见知识点的书。

如今网上有人写了一个《Effective Rust》出来，也是类似的思路。

#系统设计
《DDIA逐章精读》，配套的视频见 B站，油管。