In Dale's Proof Search Foundations for Logic Programming talk, he gives a great minimalist example of an interactive system: toggling a switch. The encoding in Forum, a logic programming language based on full linear logic, goes like this:

flip on off.
flip off on.

toggle G
    o- sw V * flip V U * (sw U -o G)

or in logic,

\[
\exists u,v.[sw\ v\otimes flip\ v\ u \otimes (sw\ u \multimap G)]
\multimap
toggle\ G
\]

(Yes, I mainly did that to test the $$\LaTeX$$ rendering script I'm using.)

The talk I linked to gives a derivation (which I won't painstakingly copy here) illustrating the execution of the program: the goal sequent $$\Gamma; \Delta, sw\ on \longrightarrow toggle\ G$$ evolves through proof search into $$\Gamma; \Delta, sw\ off \longrightarrow G$$.

But this is something of a counterintuitive, higher-order encoding. The "action" by a hypothetical user of toggling the switch must be indexed by $$G$$, the goal that continues the program. Here, the action (together with the continuation) is a logical proposition that becomes the goal clause of proof search.

If instead we did this Twelf-style, we might make "toggle" a term constructor -- a rule for proof search -- rather than a proposition (type) constructor, leading to the following encoding:

flip1 : flip on off.
flip2 : flip off on.
toggle : sw v * flip v u -o sw u.

We now need to invent a distinguished atomic goal ("end") to use this as an action on contexts:

\[
\frac
{
\Gamma; sw\ on \longrightarrow sw\ on
\qquad
\Gamma; \cdot \longrightarrow flip\ on\ off
}
\]
\[
\frac
{
\Gamma; sw\ on \longrightarrow (sw\ on)\otimes(flip\ on\ off)
\qquad
\frac{\vdots}{
\Gamma; \Delta, sw\ off \longrightarrow end}
}
\]
\[
\frac
{
\Gamma; \Delta, sw\ on, (sw\ on)\otimes (flip\ on\ off)\multimap sw\ off
\longrightarrow end
}
{}
\]
\[
\frac
{
\Gamma; \Delta, sw\ on, \forall(v,u).((sw\ v)\otimes (flip\ v\ u)\multimap sw\ u)
\longrightarrow end
}
{
\Gamma; \Delta, sw\ on \longrightarrow end
}
copy
\]

(Sorry for the horrendous formatting; perhaps typesetting derivations with \frac is not really worth it...)

Here $\Gamma$ represents the signature where we've written our rules, and the interactive choice is performed not by selecting a goal, but by selecting a rule (a term from the signature, via "copy") to prove a goal.

There's not necessarily an advantage to looking at things this way, but it is the way of looking at things that is more in line with my slogans.