Really interesting article. The idea of temporal proofs is very interesting. I especially enjoy the idea of x will eventually be y. I have often wanted a static type that allows initially null but no null assignment for similar reasons.

I found the other bugs section at the bottom pretty funny though:

> If the toolbox GUI fails to launch the prover due to NullPointerException, try closing the specification and reopening it.

There is something deeply ironic about this type of error in the gui editor for a theorem prover. It’s almost petty to even make the comment, but I guess it’s reassuring that even the sorts of people who write theorem provers have pedestrian bugs like that.