PIP News: Isabelle is Up!

Before my fall I launched a PIP (Perpetual Impossible Project).  PIPs are long-range risky undertakings that cannot be finishedPIPs contradict and subvert the very notion of tightly controlled corporate style projects: hence their manifest appeal to recusants like myself.

I won’t go into details about my particular PIP. Let’s just say it captures every delusional notion I have ever entertained. Part of my project involved installing a few Proof Assistants. Proof assistants are programs that verify formal mathematical proofs. There are many proof assistant programs available. These programs are not mathematical magic bullets. They don’t prove theorems and they don’t make the job of “theorem proving” easier. To use a programming analogy: a traditional proof is like pseudo code while a formal proof is like an assembly language program.  If you have ever written a nontrivial assembly language program you have some idea of the sheer effort required to produce a formal proof.

So, if formal proof only makes mathematics more difficult, why bother? This is like asking, so if implementing pseudo code only makes programming more difficult, why bother?

Isabelle 2011 on my Ubuntu box.
A screen shot of Isabelle 2011 on my Ubuntu machine. To install this program I had to convert a Windows machine to Ubuntu and install a host of Linux tools. Reaching this point represents a lot of water under the software bridge.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.