Hey There Buddo!

I’ve been in and around assembly verification for a while now.

There is a neat paper https://arxiv.org/abs/math/9405205 Seven Trees in One, where it is shown that there is a nice isomorphism between 7 trees and one tree.

I’ve been tinkering on a solver-oriented interactive proof assistant as a library called Knuckledragger https://github.com/philzook58/knuckledragger .

Algebraic effects are a style / mathematical framework for modelling mutation, search, and some other things.

I’ve been trying my hand at translating a reasonable subset of TLA+ into z3py for the purposes of connecting specs to Verus, CBMC, and my assembly checker and also for maybe a little interactive theorem proving as a treat.

I have been writing posts about Lifting Egraphs video as an intriguing way of adding variables and scope into an egraph.

One thing I’ve been discussing with Rudi, Michel and Max is union find annotations.

I was invited a few months ago into discussions with Cheng Zhang, Sam Coward and Alexandra Silva on some work integrating loopy infinite streamy things into e-graphs.

I submitted a talk to the EGRAPHS workshop and it was accepted!

Automated reasoning is fun.