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 t

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.