有没有对“逻辑学”和“类型论”感兴趣的？

推荐试试 lean4 在线游戏 https://adam.math.hhu.de/ 的 A Lean Intro to Logic https://adam.math.hhu.de/#/g/trequetrum/lean4game-logic 和 Reintroduction to Proofs https://adam.math.hhu.de/#/g/emilyriehl/reintroductiontoproofs 两个章节。

尤其是类型论，非常适合喜欢 TypeScript 或 C++ 类型推导的强迫症患者。有些关卡很烧脑，但尽量不要搜答案或问 AI ，自己想出来会非常有成就感~

虽然 lean4 原用于数学证明，但根据“柯里-霍华德同构”（ Curry-Howard Isomorphism ），计算机程序与数学证明本质上是同一件事。有兴趣的可以试试~ 前面的入门题目很容易，后面关卡会难一点，每天挑战一题，大约一两周就可以通关。

我觉得，计算机程序是数字电子，数学证明，是模拟电子。

CPU 是数字型，但给 CPU 供电的主板，vrm 模块，确实模拟电子。
CPU 预测接下来有大动作，要求大功率，VRM 给了大功率，大电压，结果 CPU 因为缓存 miss ，导致计算任务其实很小，
那电已经来了，怎么办，只能靠 vrm 来泄压。而且，电压变动，会导致波动，出现 undershoot 和 overshoot ，所以有了 CPU 缩肛。

还没看 op 的网站。

看标题点进来，原以为你要讨论的是哲学。。。

德文的网站,应该不是楼主大神的.
我玩了一下,以前就有人说类似楼主这种大神,天天写大家看不懂的代码,玩看不懂的游戏,现在总算是切身感受到了.。