TD4 4位DIY CPU组装与编程完全指南
作者购买并组装了TD4这款4位DIY CPU套件。文章详细记录了焊接过程中的坑（如二极管方向、USB接口焊接顺序），深入解析了CPU内部原理（地址解码、指令集、寄存器、进位触发器等）。作者还分享了从简单LED闪烁到复杂上下计数程序的编写过程，并提供了自己写的Python汇编器和模拟器代码。最后提到了Nand2Tetris课程和Ben Eater项目作为延伸…
Hey There Buddo!
Philip Zucker 的博客，关于编程、数学、逻辑与物理的技术写作。
文章
域、循环项与扁平方程系统
作者介绍了近期与Cheng Zhang等人关于将循环无限流式结构整合进e-graphs的讨论，并回顾了自己几年前在类似方向（coegraph）的工作。涉及前沿的图论与代数系统交叉研究，具有较强的一手交流性质。
提升 E-Graphs：一篇被 PLDI 2026 接收的论文
作者宣布其关于 Lifting E-Graphs 的论文被 PLDI 2026 的 EGRAPHS Workshop 接收。这是一个重要的学术认可信号，E-Graphs 是当前编译器和程序分析领域的热点话题，具有较高关注度。
从 eprover 读取证明对象与重写系统至 Knuckledragger
讲述如何将自动化推理工具 eprover 生成的证明对象和重写系统集成到 Knuckledragger 中。属于自动化定理证明领域的工程实现细节，适合对该领域感兴趣的开发者。
面向家庭的Python FrozenSet依赖类型理论
作者表达了将抽象事物“有限化”并放入日常框架（如Python的Frozenset）中处理依赖类型理论的尝试。这是一种将高阶类型理论与具体编程语言特性结合的个人实验性观点。
使用 Dump Calculus 进行函数的提升与降低
作者探讨如何构建无名 De Bruijn e-graph，并由此引出用于函数提升和降低的组合子设计。这是一篇涉及底层编译器理论、图重写系统和函数式编程组合子的深度技术思考，适合对形式化方法和 e-graphs 感兴趣的工程师。
为 Alpha 等价性简化/提升 E-图：第一阶段检查点
作者正在构建支持 Alpha 等价性的 e-graph（E-图）。在实现过程中，发现原本以为复杂度会失控，但随着理解加深，代码反而变得更简洁。本文是该项目的阶段性检查点记录，分享了从复杂到简化的认知过程。
带 Thinnings 的 Alpha 等价哈希共享
探讨在 egraph 技术中引入 thinnings 以实现 Alpha 等价哈希共享的技术步骤。这是编译器优化和符号计算领域的一个具体算法改进点。
Monus、Factor与稀疏并查集发现
作者分享了一种思考广义e-graphs或模理论的“食谱”，核心思路是将常规的并查集（Union Find）替换为某种广义的并查集概念。这是关于底层数据结构与等价关系建模的工程/理论探索。
使用 Knuckledragger 对 RISC-V 汇编进行细化建模与验证
介绍使用 Knuckledragger 工具对 RISC-V 汇编进行细化建模和验证的方法。Binary verification 在底层系统开发中有实际用途，涉及具体的形式化验证技术路径。
Thinnings：子列表见证与 de Bruijn 索引移位聚类
作者受 Mastodon 上 Conor McBride 关于 Thinnings 的讨论启发，认为这是首次见到去除了复杂理论包装的直观解释。这一概念帮助作者理清了思路，并激发了关于 Lambda Egraphs 和广义并查集的大量新想法，计划后续深入展开。
把 SMTLIB 当作编译器中间表示(IR)：SSA 即函数式编程的工程实践
作者提出利用 Z3 SMT 求解器的 AST 直接作为编译器中间表示(IR)。核心观点是 SSA 形式与函数式编程高度同构，通过将控制流图(CFG)的每个块映射为递归定义的函数，并利用 SMT 的 substitute_funs 进行展开和简化，从而在逻辑层面实现编译优化和验证。文章展示了从 Python 代码到 SMT 定义再到类汇编 IR 打印的完整转…