Re: Some user feedback

[Çağatay Kavukçuoğlu <cagatay.k...@xxxxxxxxx>]

I've recently started using TLA+ and the toolbox; my experiences have some commonality with James's. 

I have found the hyperbook to be a good tutorial to start learning. I find that the math syntax is in most cases easier to understand and more expressive than plain ASCII text could hope to be; the PDF format definitely has that as a positive. On the other hand, I soon came to miss the ability to bookmark and search as I'm used to on the web, and I found Acrobat Reader to be fairly user hostile software in terms of usability. I think that given the documentation toolchains available today (Jekyll/Sphinx for building the docs, MathJax for typesetting, MultiMarkdown for authoring, Dash/Zeal/Velocity for offline docsets) and the current state of browser technology, HTML is a lot more feasible today that it would have been ten years ago. If the sources for the hyperbook and the PlusCal manual are available publicly with a creative commons license the community can experiment with pulling the documentation into a new form.

As I spent more time with TLA and PlusCal, the fractured nature of the documentation became a bigger hassle for me. I'm essentially dividing my attention between the Specifying Systems book, the hyperbook and the PlusCal manual. They are written clearly and I enjoyed reading them, but each of these have topics that only one of them covers, and they also repeat a significant deal of information between each other. One of the things that I hope would come out of an effort to improve documentation is one authoritative set of documents that can serve as a tutorial, user's guide and manual. As things stand today, it's easy for a newcomer to feel frustrated at the effort it takes to simply find the relevant information on how some feature works. For example, the Specifying Systems book explains recursive functions, but the hyperbook clarifies that TLA+ 2 has recursive operators as well, and the PlusCal manual explains how recursion works in that language. This topic would be better exposed under a single heading covering all cases in the ideal documentation. Similarly, various TLA expressions are explained in the PlusCal manual and the hyperbook, but only Specifying Systems book has the formal semantics of what TLA expressions entail and other important details such as how exactly TLC values are compared to each other. 

I'm a lot more positive about the emphasis on providing the toolbox; the integrated environment is an overall plus and helps a lot during debugging. The one thing I intensely long for is a REPL; the lack of an environment that I can use to build models incrementally with immediate feedback, in a language such as TLA+ (which would lend itself so well to it) makes me sad. I'm aware of the "evaluate constant _expression_" feature in the toolbox, but that is a clunky substitute a long way off from the seamless experience of a REPL.

In the last few months I've spent with it, I've found TLA to be a surprisingly useful tool that changed how I write software; thanks for making it available and working on it persistently. My efforts to sell it to colleagues would definitely be helped by a better website and consistent, online documentation. 

CK. 

On Thursday, November 20, 2014 7:11:24 PM UTC-5, Leslie Lamport wrote:

Hi James,

Thanks for taking the time to write up your feedback.  And thanks also
for your offer to try to help solve some of the problems you found.  I
hope we'll be able to take you up on your offer.

Before getting to specifics, I want to say that I believe your desire
for the command-line interface to come first represents a small
minority view in the general programming community.  Gerard Holzmann,
the inventor of the Spin model checker, told me a while ago that when
he put a very simple GUI on Spin, the number of users increased by an
order of magnitude.  I have had a number of comments that the Toolbox
does not provide the power they have come to expect from the IDEs they
use to write programs.  Although others have complained about the
absence of good documentation for the command line interfaces, no one
else has ever said that the Toolbox should not be the principle method
of using the tools.

However, I have not based my career on copying what other people do.
I have always tried to find what works best, regardless of what others
think should work best.  I'm not a fan of screen flash.  I started
programming before there were even command-line interfaces.  I use
whatever I find most convenient.  For example, for manipulating files
I will use either the Windows File Explorer GUI or a Cygwin
command-line shell depending on what I'm doing.

If you think running the TLC model checker from a command line could
be better than running it from the Toolbox, then you do not appreciate
all that you can do from the Toolbox--perhaps because you have just
been writing simple specs and have not yet had serious debugging of
specs to do, and perhaps because of poor documentation.  And only a
blind person could prefer running the prover from a command line
rather than from the Toolbox.  (We don't have the resources to try to
provide interfaces for disabled people.)

So, we are not going to spend resources trying to improve command-line
interfaces.  However, they should be documented better than they are.
That's one of the many things I haven't had time to do and am not
likely to find time in the near future.  But the information is easily
accessible, so it's not rocket science.

I'm willing to devote some energy to helping someone produce better
documentation for the Toolbox.  I would appreciate any help you can
provide.  I suggest that you start by reading the Toolbox's help pages
and tell me what can be done to improve them.  What I would like is to
have the Toolbox read the user's mind and, when she doesn't know what
to do next, present her with the appropriate help page.  I don't know
how to implement that.  Simply presenting the information in a single,
logically structured document doesn't seem to work very well.  25
years ago I found that LaTeX users weren't very good at reading the
manual, and people have gotten a lot less willing to read than they
were then.

You wanted HTML documentation.  There are two things that need to be
documented: TLA+ and the tools.  I considered alternatives to
LaTeX-produced pdf when I started writing the Hyperbook.  HTML would
have been ten times harder to use to produce something that was a
tenth as good.  As for the "pretty-printed" version versus the ASCII,
a TLA+ user at Intel wrote that one of the good things about TLA+ is
that if he doesn't understand what a TLA+ construct means, he can
look it up in a math book.  Math books don't write math in ASCII, they
use standard mathematical symbols.  I want TLA+ users to think in
terms of math, which means thinking in terms of its symbols.  You will
soon get to be bilingual, reading math and its TLA+ ASCII versions
equally well.  And if you learn TLA+ by reading the Hyperbook, you
will find that the ASCII versions are all sitting there for you to
just copy into the Toolbox.

By the way, I believe the Hyperbook has a page with a table of ASCII
<-> Math translations.  It's part of the few-page summary of TLA+ in
Specifying Systems, which is also available as a separate pdf file.

As to the zip file, the only way to write hypertext in pdf is with
hundreds of separate files.  You want those files on your own machine;
you don't want to have to be going out over the web for every pop-up.
I don't know any alternative to a zip file.

As to documenting the tools, there seem to be two issues: the
mechanics of the various bells and whistles that the Toolbox provides,
and the more subtle issues that involve understanding TLA+.  For the
latter, the Hyperbook seems to be the best medium.  The former is what
the help pages try to document, but don't seem to be doing a good job.

Leslie