I use Isabelle, even though it’s only in a hobby / side project fashion. But I have to say, the jEdit GUI is great. When you first see it, it looks a little outdated and clunky, but after using it for a while it has really, really good UX. Like inspiringly good.
The source of the goodness is that it’s extremely responsive, and almost everything can be interacted with in real time. The main thing Isabelle (and most other proof assistants) help you with is the proof state. Proofs are logical arguments that consist of multiple steps, and Isabelle exposes each of these steps to you, and allows you to interact with it. I’ve heard this is only possible because the UI is highly concurrent, and does a lot of work in the background while you can move around and view all different parts of the proof state.
It’s like a REPL for proofs, but because it’s graphical there are multiple different things going on at once vs. just one request / response. It’s a surprisingly great UI.
I use Isabelle, even though it’s only in a hobby / side project fashion. But I have to say, the jEdit GUI is great. When you first see it, it looks a little outdated and clunky, but after using it for a while it has really, really good UX. Like inspiringly good.
The source of the goodness is that it’s extremely responsive, and almost everything can be interacted with in real time. The main thing Isabelle (and most other proof assistants) help you with is the proof state. Proofs are logical arguments that consist of multiple steps, and Isabelle exposes each of these steps to you, and allows you to interact with it. I’ve heard this is only possible because the UI is highly concurrent, and does a lot of work in the background while you can move around and view all different parts of the proof state.
It’s like a REPL for proofs, but because it’s graphical there are multiple different things going on at once vs. just one request / response. It’s a surprisingly great UI.