gistfile1.txt

Learning https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/
Notes on the UI:

There's no sandbox that'd let you explore creating new theorems.
(I was stuck on one in Multiplication World but thought I'd be able to
prove a variation with the expressions commuted, (a+b)*t = a*t + b*t.
Hopefully that'd help me get unstuck.)

There are 4 panes (names mine):
  Docs            Editor                  State
    tactics         instructions            environment at the cursor in the proof
    theorems        in-progress proof
                                          Messages
                                            error or warning

The central activity is adding a step to a proof.
You do that by looking at the state, finding an applicable tactic/theorem, and typing it in.
But the state pane is maximally distant from the tactics/theorems pane.

When you start typing, the state goes blank right away, even though
you might want to consult it as you type.

After about a second it updates (to an error message, unless you're already done typing).

The same info is typically repeated in the State and Messages panes.

Most-desired changes:
- The state at the point of the first error remains readable, just colored differently or something.
- During update, the state display isn't erased while that's being computed, just recolored or something.
- Update is <100 msec, or anyway quick enough to not feel like a drag.

Further wishlist:
- Make State/Messages less redundant. My eyes tend to stray to the redundant info when it updates.
- The in-progress proof may need a scrollbar to see it all. Can it expand instead? Or just be bigger?
- It'd be neat to hover over bits of the state and have applicable tactics pop up to be clicked on.
- Maybe move Docs to the far right?
- Edit the function declaration, not just the in-progress proof. (Normally only in a sandbox.)
  What if this whole thing could be a wiki?

Of course there are also questions of language design: a list of tactic steps is not very readable.

Or a from-scratch gamelike experience:
See toontalk for some inspiration.
But you'd want to have 'holes' ("... and then a miracle occurs") and easy scrubbing back and forth in time.