I'm doing okay, although still feeling buried in work, and not fantastically productive. Thanks to everyone who wrote with concern, and sorry for not responding to your email.

I spoke with David McCusker quite extensively yesterday. It's possible that Fitz will prove a good fit with the goals of the OSAF, which would be fun. I think I'll be visiting them soon.

In any case, it's clear that a working prototype of Fitz is on the critical path to everything else, so I'm going to try to get that done next.

Proofs

For fun, I proved the ordered pair theorem for (nonnegative) natural numbers in Metamath. It's a very low-level framework, so a lot of aspects are tedious, but overall I was pleased with how it turned out. This is actually my first experience proving something completely rigorously. I recommend it to others.

I've been having a great email discussion with Norm Megill and Robert Solovay, and also with Josh Purinton. Very cool.