作者在其低门槛 Python 证明助手knuckledragger中对重载、类型类和代数层次结构等进行了探索和实践，主要内容如下：

• 层次结构与转换：knuckledragger有 Python 编程（“编译时”，静态，元）和 z3 表达式（“运行时”，动态，对象）两层，可在两者间转换，类似 Python 生成 C 代码或 staged 元编程，如Forall量词可在“编译时”展开或让 z3 处理。还有其他层次，如 wacky Python 元编程和元类、Python 类型、类定义、类实例、普通 Python 函数、z3 排序、z3 表达式、Proof 等，各层在设计和实现中存在关联和困惑。
• SortDispatch：knuckledragger早期就有 SortDispatch，是functools.singledispatch的变体用于重载，通过注册支持的类型和__call__实现根据第一个参数的类型查找相应函数，其注册字典模式在多个机制中常见，如functools.cache。在支持运算符重载时，考虑过多种方式，如创建新类、浅嵌入 z3 排序到 Python 类型系统、将 z3py 表达式包装为数据成员等，最终选择了 SortDispatch 来处理基于z3.SortRef的重载。
• Dataclasses：作者喜欢 Python 的 dataclasses，可定义结构并获得默认行为，类似模块系统，Python 子类化类似包含机制。在knuckledragger中，dataclasses 可用于聚类属性，如定义Semigroup和Monoid等类，但 Python 类型检查在这方面存在不足，__post_init__函数可检查传入数据的正确性。同时，可通过smt.And捆绑多个kd.Proof，但缺乏好的命名方式。
• GenericProof：GenericProof是一个轻量级机制，用于在 z3 逻辑中无法量化的情况下对参数化数据进行证明。它通过将 lambda 推到 turnstile 右侧，利用 Python 元 lambda 来实现，通过初始化时的函数检查传入参数的正确性，与类型类有相似之处。
• TypeClass：人们对类型类爱恨交织，作者从 Oleg Kiselyov 的讨论中获得灵感，类型类可记录基于类型的信息，可在用户级别实现或在 staged 元编程系统中运行。TypeClass的构造函数通过键从注册中心获取信息填充实例，可添加可扩展的rules字段，目前设计尚未稳定。
• Z3 Parametric Types：Z3 最近获得了对参数化类型变量的初步支持，但仍处于不成熟状态，作者需要一些通用机制来实现临时多态或参数化其他不可内部化的数据。参数化类型是 Z3 对象逻辑与 Isabelle HOL 或 HOL Light 的主要区别，也是导致像 boogie、why3 等分离元层的原因。
• 其他方面：作者提到可将 GenericProof、SortDispatch 和 TypeClass 统一为一个超类，认为不应将 Python 类型和 z3 排序混淆，证明对象在 Python 层，可将相关证明捆绑到 Python dataclass 中。不同系统对“类型”有不同的含义和处理方式，如依赖类型理论系统刺破了元障碍，而 Coq 和 Lean 也有各自的特点。每个Sortdispatch维护一个字典映射第一个参数的排序到专门的函数，浅嵌入类型系统有局限性，SMTLib 接近函数式编程语言，可对其进行部分求值等尝试，还可定义抽象排序并进行相关证明操作等。