[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: Some user feedback

Hi Leslie,

  >>Your REPL seems to be a specification editor based on the TECO model,
  >>treating the screen as a glass teletype.

It's more than that, because of
   - the ability to very easily evaluate expressions at any time, using the definitions you've built up so far.
   - the speed of iteration (including staying focused on the keyboard, rarely using the mouse).

I agree that from the outside it looks like it could be a step backwards. But I suspect that fans of REPLs would claim that the resulting experience is more than the sum of its parts.

As I said, I don't have a strong personal need for this, because I use ASSUME commands to evaluate expressions using definitions I've built up so far, and I've learned to live with the current speed of iteration. (The speed of iteration seems to be a bit better since I recently switched to using a laptop with an SSD and more ram.) An improved 'logic/_expression_ calculator' would be very nice, but not at the expense of the other things I listed.

However, I do know some programmers who really like working in a REPL; they describe it as being more intense and immersive than the conventional edit/compile/debug cycle. A REPL may or may not produce better end-results for them (I have no idea), but it does involve a different style of interaction with the tools. As long as the style of interaction with the tools does not interfere with thinking mathematically then it seems like a matter of personal preference in user interface. I expect that we'll see a broader spectrum of personal preferences as TLA+ gains adoption among new groups of people.

I should mention that there are many forms of modern REPL.  E.g.
   "You can think of it like a pretty REPL that can plot graphs and draw tables, or you can think of it as an editor for rich documents that can contain interactive Clojure code, graphs, tables, notes, LaTeX formulae."

My own speculative personal preference for user-interface would be for something closer to Don Knuth's 'Literate Programming' system. I'd like to write a spec "in order of clearest explanation" (as Knuth says), primarily in prose like a technical paper, then refining the prose into formal definitions. I'd then like to have the spec automatically rearranged into the form necessary for the model-checker (basically macro-expansion). This reflects how I work now, but I'm currently lacking the automated tool or the ability to maintain both versions. I've mentioned this in several talks (e.g. [2]) but haven't had time to try writing or adapting a tool[1].


[1] http://www.literateprogramming.com/tools.html
[2] From slide 22 of http://tla2012.loria.fr/contributed/newcombe-slides.pdf
         Donald Knuth wrote
“Some of my major programs ... could not have
been written with any other methodology that I’ve
ever heard of. The complexity was simply too
daunting for my limited brain to handle; without
literate programming, the whole enterprise would
have flopped miserably.”
“Literate programming is what you need to rise
above the ordinary level of achievement"

On Mon, Nov 24, 2014 at 1:19 PM, Leslie Lamport <tlapl...@xxxxxxxxx> wrote:

Hi Chris,

You write that a REPL should:

 - Allow ... constants and variables to be declared.

 - Allow operators to be defined and re-defined...

 - Provide a command to display the definition of any symbol. 

A set of declarations and definitions is a specification.  I therefore
infer that a REPL would maintain a Current Specification that is
modified and viewed by command-line commands.

The first text editor I can remember using was called TECO. In those
days, video displays were too expensive for common use, so one
interacted with a computer using a teletype-style device with a
keyboard and a roll of paper.  TECO maintained a current cursor
position, and one edited a file by keyboard commands to move the
cursor and to insert or delete characters at the cursor position.  To
see the actual contents of the file, you executed a command to print
part of it--usually a few lines containing the cursor.  When CRT
displays became common in the 1970s, they were first used as "glass
teletypes", treating the screen as a virtual roll of paper.  People
soon switched to visual editors that made the screen a window on the
file that you edited visually--e.g., Emacs (which was first built on
top of TECO). 

Your REPL seems to be a specification editor based on the TECO model,
treating the screen as a glass teletype.  (Instead of viewing a few
lines around the cursor, the user displays an individual definition.)
However, unlike text files, specs have a logical structure.  So, what
happens if you try to add a syntactically incorrect definition?  One
possibility is to produce a syntactically incorrect spec, which you
then fix by actual TECO-style editing commands.  However, I presume
that you intend the definition command to fail, so the user would have
to issue a whole new command to add the definition.  Since you are
using a virtual paper roll rather than real paper, this is not hard to
do with copy/paste/edit starting from the incorrect command.

People who want a REPL interface apparently think it's a great step
forward to return to the 1960s.  I lived through the 60s and I don't
think they were that great (except for the music).  So, I will have no
part in implementing a REPL interface for TLA+.  If I want to edit a
Current Specification, I will do it by putting the specification in a
buffer and editing it with something like Emacs, not something like
TECO.  And TLA+ already provides a syntax for displaying a
specification in that buffer.

I couldn't tell if the Current Specification in your proposal is
actually what the Toolbox thinks is the current spec, so your REPL
command to modify a definition actually changes the .tla file.  I
suspect it isn't.  In that case, the Current Specification should have
its own buffer.  This allows you to play with potential changes to the
spec--or make changes just for debugging purposes--without affecting
the official spec.  There are any number of ways of doing this--for
example, with an easy to use repository.  With a REPL, if you want to
change a definition in the spec to a modified version that you've
since changed, you will have to search back in the scroll for the
command that created it.  With a repository, you could make lots of
checkpoints and go to the appropriate one.  Another alternative is to
create new models instead of new checkpoints.  As part of a model, the
Toolbox keeps the entire spec that was last checked by the model.  I
believe you can open that spec in a read-only editor, but I don't
remember how.  (I've never used it.)  But it should be easy to add
Toolbox commands to allow the user to edit that saved version and
rerun TLC on it.

 - Allow a key-press (presumably Ctrl-C) to promptly interrupt a
   long-running evaluation.

That shouldn't be hard to add to the Toolbox, if clicking on a button
is too much work.  Since you can have more than one model executing at
a time, there might be some problem in determining which one gets

 - Allow explicit temporary local binding (shadowing) of constants and
   variables, to test operators.  This would only be allowed in commands
   that did not have side-effects.  i.e.  It would not be allowed when
   defining or redefining a symbol.

I don't know what that means.  A model requires you to "bind" CONSTANT
parameters and allows you to redefine defined operators.  Presumably you
have something else in mind.

   My recollection is that output from Assert(_,_) and PrintT(_) of
   complex nested structures would occasionally be so hard to read that I
   would copy/paste it into a text editor and manual reformat it a bit,
   to clarify a problem.

Your recollection is probably correct.  I have to do that sometimes.
No pretty-printer can automatically display a complex value the way I
want to see it because how I want to see the value depends on what I'm
looking for.  So I might want the same value to de displayed in two
different ways.  Mark's algorithm is not very sophisticated, so it can
probably be improved.  But I doubt if it will be easy to make it very
much better.

   Using TLC currently requires using the mouse quite a lot, whereas
   using TLAPS can be done mostly from the keyboard.

There are many more things you can do with TLC than with TLAPS, so
doing everything with keyboard commands would be pretty complicated.
However, I believe that once a window is selected, any click of a
button on that window could be implemented as a keyboard command.  I
don't know how to attach keyboard commands to individual windows.
Anyone who knows how can easily do it; they just have to coordinate
with me.



You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.