围绕一个问题持续积累的阅读、笔记与实践路线。
从类型约束、性质测试与模型检查，走向 Coq 和 Lean 4 中机器可检查的证明。
从函数式编程进入范畴论，沿着 Bartosz Milewski 的视频与已有笔记继续探索。