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.
Groxx•1mo ago
Every theorem prover tool I've used has been an absolute nightmare of UX¹ and flaky installs and random broken things, so yea. They definitely have bugs like that, and for some reason it's particularly frequent :|
It's not enough to make it not useful, not by a long shot. So everyone uses them. But it's a gigantic turn-off for anyone getting started or looking into it semi-casually, I suspect it's harming the field more than they think.
1: I don't mean like "ew everything's crammed together, give it some liquid glass and let the components breathe", that would be awful and TCL/TK components are plenty functional. I mean like "sometimes when you configure your initial axioms, the text field will not let you enter any text". Or "clicking 'save' will do nothing until you close and relaunch". Or on some OSes the cross-platform UI toolkit from two decades ago will overlap controls. Or it will simply crash 12% of the time when you view one settings section. Or "to get any syntax errors while trying to learn the system, you need to set up your initial axioms in a settings pane 3 layers deep with no field label, but nothing will tell you to do this, it will just act like a plain text field and the run button will be grayed out with no tooltip". The absolute bottom of the UX-barrel.
MobiusHorizons•1mo ago
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.
Groxx•1mo ago
It's not enough to make it not useful, not by a long shot. So everyone uses them. But it's a gigantic turn-off for anyone getting started or looking into it semi-casually, I suspect it's harming the field more than they think.
1: I don't mean like "ew everything's crammed together, give it some liquid glass and let the components breathe", that would be awful and TCL/TK components are plenty functional. I mean like "sometimes when you configure your initial axioms, the text field will not let you enter any text". Or "clicking 'save' will do nothing until you close and relaunch". Or on some OSes the cross-platform UI toolkit from two decades ago will overlap controls. Or it will simply crash 12% of the time when you view one settings section. Or "to get any syntax errors while trying to learn the system, you need to set up your initial axioms in a settings pane 3 layers deep with no field label, but nothing will tell you to do this, it will just act like a plain text field and the run button will be grayed out with no tooltip". The absolute bottom of the UX-barrel.