### Logic with a black tie and tails

I've had lots of fun with formal logic and theorem provers. This
is a partial list of what I have done.

#### PVS

Just after graduate school, when I was working at the University of
Kansas, I discovered PVS, a
formal verification system. PVS lets you write a formal
specification of a system, then prove theorems about that system.
After learning my way around the system, I made a number of
contributions, including:

- Ported PVS's BDD package
to 64-bit machines, as 64-bit builds were starting to become common
at the time.
- Ported PVS to SBCL. Prior to that, it only ran on
Allegro Common
Lisp, a commercial product.
Some work
had already been done on porting to other lisps, but I got PVS to
run on a second Lisp for the first time. To be fair, Sam Owre had
to do a fair amount of work on top of my port before the bugs were
really ironed out.
- Contributed theorems to the
PVS prelude.
Just search for my name in there.
- Contributed theorems to the
NASA
PVS Library. You can see the collections to which I
contributed
here.

#### Metamath

My use of PVS petered out around 2007. Fast forward to 2016. After
reading an article about
metamath, I decided to give it
a try. It's fun! I've been formalizing the material in N. J.
Cutland's book, **Computability: An introduction to recursive
function theory**. I've gotten through Definition 2.3 on
page 27, in chapter 2. If you would like to see it, look
here. This is based on the develop branch of
the set.mm git
repository, on top of commit 270904b9443d8c2843cfd5c7cb7c86025f8e29c0
by David Wheeler on Tuesday August 29, 2017.