好资源和短想法
我一直都在用Linux的命令行，要么用ansible和fabric来批量管理自己的Linux服务器。前几天看到AI火火兔的玩家在用 1Panel 部署 Docker 镜像，我试了试 1Panel，确实很方便，使用 1Panel 能大大降低 Linux 服务器的使用难度。于是我又录一个部署的视频，用1panel来部署folotoy，用的Windows操作的 ：https://youtu.be/89paeh35qBA
#编程语言
Daniel P Friedman在编程语言界的贡献
转自微博：https://m.weibo.cn/status/4952639604523552
因为最后一段文字，特地找了王垠的两篇文章：
* 《写小人书的老顽童》
* 《Chez Scheme 的传说》
------ 分割线，以下为原文 ------
绝对是今年计算机专业的一件大事。Daniel P Friedman，79岁高龄，在2023年出版了他的The Little ... 系列的新书，The Little Learner。
老爷子是Lazy Evaluation的发明者，Scheme届一哥，发明Scheme的人都亲口承认这一点；现在还在Scheme届抗梁的人物，除了UBC那个发明Aspect Oriented Programming、MIT肄业、Xerox Parc精英Gregor Kiczales之外，全是Friedman的徒子徒孙；因为Scheme是最接近Lambda的语言，所以Friedman可以理解为能写『顶尖』代码的Church。『顶尖』二字在这里的意思不但指它在学术界的编程能力是顶流，他给Scheme语言留下的诸如Pattern Matching宏代码可以正面刚Kernel里的所有工业代码。
不止Scheme语言教学。Friedman的同事，另一个传奇人物Kent Dybvig，写了工业级的Scheme语言编译器，Chez Scheme，包括Cisco在内的很多大企业都是他的客户。Chez Scheme后来出现了开源的版本，在这个版本里Friedman和Dybvig合作了被称为nanopass的编译器框架；虽然Scheme不是流行的工业语言，但是两个版本的Chez Scheme在编译速度和执行速度上都可以跟任何工业级语言编译器抗衡；而且Chez Scheme自带的解释器，性能高达编译器的1/2.5的水平，想想v8出现时直接把JavaScript速度提高了1000-5000倍，这个名称为Petite Chez Scheme的解释器毫无疑问是性能最好的编程语言解释器。
远不只这些。
The Little Typer，是介绍Dependent Types的入门书籍，提供了仅6000行代码实现的Pie语言；任何人都可以从这里开始了解现代计算机语言的类型系统。
The Little Prover，通过ACL2定理证明器讲解现代定理证明器使用。
The Reasoned Schemer，仍通过Scheme语言讲解relational logic和logic programming。这本书神奇的出到了第二版，令人匪夷所思，因为这实在是非常冷门的领域。该书的第二作者William E. Byrd是Friedman的学生，他在Youtube上有故弄玄虚的视频讲解他当年看到Friedman的代码时，是如何获得了被天打雷劈的感受的。
++++
以上都是符号主义在编程领域的巅峰之作。
我承认我会因为Frank Pfenning（Peter Andrews的学生，Alonzo Church的徒孙），Robert Harper（Robert Constable的学生，Stephen Cole Kleene的徒孙，Alonzo Church的曾徒孙），Steve Awodey（Saunders Mac Lane的学生，Mac Lane是Weyl和Bernays的学生，前者是Hilbert的学生，后者是Landau的学生）等人的学术成就，把他们的学术水平看在Friedman之上，这三个人是cmu三剑客，活跃在youtube上的oplss频道，讲解constructive logic, type theory和category theory。但是如果没有Friedman，你将只会淹没在符号和数学里，远没有现在这样容易只通过一种语言了解计算机科学的如此广阔的领域。
而他在79岁这一年，出版了The Little Learner，关于Deep Learning，给这本书写序的人是MIT的Guy Lewis Steele Jr.（Gerald Jay Sussman的学生）和Peter Norvig（人工智能：一种现代方法的两个作者之一）。
无法表达对老爷子的敬佩之情，不把这些书的习题都做了，都对不起他老人家。
++++
王垠写过不少盛赞Dybvig和Friedman的文字，他是令人羡慕的看见过光的人，但不知道为什么他拿着手电筒离开了印第安纳。
Daniel P Friedman在编程语言界的贡献
转自微博：https://m.weibo.cn/status/4952639604523552
因为最后一段文字，特地找了王垠的两篇文章：
* 《写小人书的老顽童》
* 《Chez Scheme 的传说》
------ 分割线，以下为原文 ------
绝对是今年计算机专业的一件大事。Daniel P Friedman，79岁高龄，在2023年出版了他的The Little ... 系列的新书，The Little Learner。
老爷子是Lazy Evaluation的发明者，Scheme届一哥，发明Scheme的人都亲口承认这一点；现在还在Scheme届抗梁的人物，除了UBC那个发明Aspect Oriented Programming、MIT肄业、Xerox Parc精英Gregor Kiczales之外，全是Friedman的徒子徒孙；因为Scheme是最接近Lambda的语言，所以Friedman可以理解为能写『顶尖』代码的Church。『顶尖』二字在这里的意思不但指它在学术界的编程能力是顶流，他给Scheme语言留下的诸如Pattern Matching宏代码可以正面刚Kernel里的所有工业代码。
不止Scheme语言教学。Friedman的同事，另一个传奇人物Kent Dybvig，写了工业级的Scheme语言编译器，Chez Scheme，包括Cisco在内的很多大企业都是他的客户。Chez Scheme后来出现了开源的版本，在这个版本里Friedman和Dybvig合作了被称为nanopass的编译器框架；虽然Scheme不是流行的工业语言，但是两个版本的Chez Scheme在编译速度和执行速度上都可以跟任何工业级语言编译器抗衡；而且Chez Scheme自带的解释器，性能高达编译器的1/2.5的水平，想想v8出现时直接把JavaScript速度提高了1000-5000倍，这个名称为Petite Chez Scheme的解释器毫无疑问是性能最好的编程语言解释器。
远不只这些。
The Little Typer，是介绍Dependent Types的入门书籍，提供了仅6000行代码实现的Pie语言；任何人都可以从这里开始了解现代计算机语言的类型系统。
The Little Prover，通过ACL2定理证明器讲解现代定理证明器使用。
The Reasoned Schemer，仍通过Scheme语言讲解relational logic和logic programming。这本书神奇的出到了第二版，令人匪夷所思，因为这实在是非常冷门的领域。该书的第二作者William E. Byrd是Friedman的学生，他在Youtube上有故弄玄虚的视频讲解他当年看到Friedman的代码时，是如何获得了被天打雷劈的感受的。
++++
以上都是符号主义在编程领域的巅峰之作。
我承认我会因为Frank Pfenning（Peter Andrews的学生，Alonzo Church的徒孙），Robert Harper（Robert Constable的学生，Stephen Cole Kleene的徒孙，Alonzo Church的曾徒孙），Steve Awodey（Saunders Mac Lane的学生，Mac Lane是Weyl和Bernays的学生，前者是Hilbert的学生，后者是Landau的学生）等人的学术成就，把他们的学术水平看在Friedman之上，这三个人是cmu三剑客，活跃在youtube上的oplss频道，讲解constructive logic, type theory和category theory。但是如果没有Friedman，你将只会淹没在符号和数学里，远没有现在这样容易只通过一种语言了解计算机科学的如此广阔的领域。
而他在79岁这一年，出版了The Little Learner，关于Deep Learning，给这本书写序的人是MIT的Guy Lewis Steele Jr.（Gerald Jay Sussman的学生）和Peter Norvig（人工智能：一种现代方法的两个作者之一）。
无法表达对老爷子的敬佩之情，不把这些书的习题都做了，都对不起他老人家。
++++
王垠写过不少盛赞Dybvig和Friedman的文字，他是令人羡慕的看见过光的人，但不知道为什么他拿着手电筒离开了印第安纳。
1989 (Taylor’s Version)
Music: https://music.apple.com/us/album/1989-taylors-version/1708308989
Spotify: https://open.spotify.com/album/64LU4c1nfjz1t4VnGhagcg?si=BWVSRdC6SLyr9_KKHKg8UA
Music: https://music.apple.com/us/album/1989-taylors-version/1708308989
Spotify: https://open.spotify.com/album/64LU4c1nfjz1t4VnGhagcg?si=BWVSRdC6SLyr9_KKHKg8UA
这个 New Repository Overview 里的快捷搜索真好用，推荐大家都开开
jvav终于终于有官方的playground了！ https://dev.java/playground/
这个新官网感觉还有很大优化空间啊，不过 oracle 居然搞了一个 .java 的顶级TLD，这个排面一下子就上去了。希望以后能开放注册吧，毕竟jvav的项目还是很多的
这个新官网感觉还有很大优化空间啊，不过 oracle 居然搞了一个 .java 的顶级TLD，这个排面一下子就上去了。希望以后能开放注册吧，毕竟jvav的项目还是很多的
大胆预测 COCOON 是今年的 Game of the Year！游戏设计/导演是为我们带来过 Inside 和 LIMBO 的 Jeppe Carlsen
https://www.cocoongame.com/
https://www.cocoongame.com/
#App
🍪 Hush：隐藏 Cookie 弹窗
🔗：Github | 官网
经常我们第一次打开一个国外网页的时候，网页总会以各种各样的形式跳出要求我们同意使用 Cookie 的弹窗。如果你也对这个征求同意的小弹窗感到厌烦，那么 Hush 可以帮上你的大忙。
✨ Features
Hush 是一个非常简单的开源 Safari 插件，兼容 Mac iPhone 和 iPad。它帮助用户隐藏 Cookie 弹窗。它不会帮助用户同意，也不会帮用户拒接 Cookie 使用，而是隐藏弹窗。
虽然产品就是这么简单，Hush 还有一个自己的网页，网页上还有示意动画。Hush 还有自己的 Product Hunt 页面。
⚙️ 开源
Hush 1.0 发布于 2020 年。目前 Hush 已经在 Github 上获得了 2.8k Star， 和 120 个 issue。Issue 大多反馈为个别网站的兼容性问题。
👀 感想
目前我使用过程中并没有碰到什么兼容性的问题。Hush 对我来说就和广告屏蔽插件一样，属于浏览器的必备工具。不过 Hush 目前只支持 Safari，相信绝大多数的读者的主力浏览器都是基于 Chromium 的，但还是推荐使用 Safri 的读者尝试一下 Hush。
频道：@NewlearnerChannel
🍪 Hush：隐藏 Cookie 弹窗
🔗：Github | 官网
经常我们第一次打开一个国外网页的时候，网页总会以各种各样的形式跳出要求我们同意使用 Cookie 的弹窗。如果你也对这个征求同意的小弹窗感到厌烦，那么 Hush 可以帮上你的大忙。
✨ Features
Hush 是一个非常简单的开源 Safari 插件，兼容 Mac iPhone 和 iPad。它帮助用户隐藏 Cookie 弹窗。它不会帮助用户同意，也不会帮用户拒接 Cookie 使用，而是隐藏弹窗。
虽然产品就是这么简单，Hush 还有一个自己的网页，网页上还有示意动画。Hush 还有自己的 Product Hunt 页面。
⚙️ 开源
Hush 1.0 发布于 2020 年。目前 Hush 已经在 Github 上获得了 2.8k Star， 和 120 个 issue。Issue 大多反馈为个别网站的兼容性问题。
👀 感想
目前我使用过程中并没有碰到什么兼容性的问题。Hush 对我来说就和广告屏蔽插件一样，属于浏览器的必备工具。不过 Hush 目前只支持 Safari，相信绝大多数的读者的主力浏览器都是基于 Chromium 的，但还是推荐使用 Safri 的读者尝试一下 Hush。
频道：@NewlearnerChannel
#课程
继续我的类型系统（当前在阅读TAPL）自学之旅，找到几个以这本书为主要教材的课程及视频：
* 北大《编程语言的设计原理》：基本按照TAPL书上的内容来讲解的，可以认为划出了每章的重点。
* cornell的CS4110《Programming Languages and Logics》：有很多TAPL以外的内容，还讲了类型系统这部分内容的数理逻辑基础。
* cornell的CS6110《Advanced Programming Languages》：还没仔细看，不知道和CS4110有什么区别。
* 油管上的一个视频课程：内容挺好的，但是貌似没有继续更新了。
除此以外，暂时这类课程好像找不到其他视频类的教程了。
继续我的类型系统（当前在阅读TAPL）自学之旅，找到几个以这本书为主要教材的课程及视频：
* 北大《编程语言的设计原理》：基本按照TAPL书上的内容来讲解的，可以认为划出了每章的重点。
* cornell的CS4110《Programming Languages and Logics》：有很多TAPL以外的内容，还讲了类型系统这部分内容的数理逻辑基础。
* cornell的CS6110《Advanced Programming Languages》：还没仔细看，不知道和CS4110有什么区别。
* 油管上的一个视频课程：内容挺好的，但是貌似没有继续更新了。
除此以外，暂时这类课程好像找不到其他视频类的教程了。