Re: [tlaplus] Some user feedback

Hi James,

Welcome to the group. I'm glad that the AWS paper was useful to you.

On this:
>>(3) realize I don't know the plaintext notation for something;
>>(4) find and open Specifying Systems PDF;

You might find it more convenient to use the very short cheat-sheet for TLA+ [1].

Page 6 of the cheat-sheet gives the ASCII versions of symbols.

On this:
>>What's the difference between a bold extential quantifier and a non-bold one?

I can say with high confidence that you will never need the bold existential or universal quantifiers (temporal quantification). The model checker doesn't support them. I've only ever them used once, in the highest levels of the Wildfire Challenge spec [2] (which BTW is a very interesting read).

There are only a handful of ASCII representations that you'll actually need in practice. There is also one rule of indentation of bulleted conjunctions/disjunctions that has occasionally tripped me up [3]. (Leslie has since documented that point in the hyperbook.)

If you use PlusCal there are a few points of syntax (in particular around fairness & termination) that are quite easy to forget. But I'm sure I would remember them if I used PlusCal as often as I use programming languages.

>>TLA+ needs to put plaintext first. In the programmer's world, plaintext is an undisputedking.

I'm a programmer too. In my case, I found the ASCII notation for TLA+ very unfamiliar (not having used LaTeX before learning TLA+), but easier to learn the numerous arbitrary quirks of various programming language. E.g. Perl, C++, Erlang, Clojure, Haskell all have odd syntax in places (including escape sequences).

The biggest problem I encountered in learning and using TLA+ was to re-wire my brain to think mathematically (e.g. declaratively) about computation and properties. That problem far exceed any transient hiccups with syntax or tools. But that re-wiring of my brain turned out to be one of the biggest benefits I've received from TLA+.

>>TLA+ needs to put the command-line tools first: in the programmer's world, command-line tools are how we interact with our files.

Your opinion is valid of course (by definition). But programmers are a varied bunch, with different perspectives. I've helped perhaps 15 programmers learn TLA+ now, and they've all been sufficiently happy with the IDE that they haven't even asked about command line tools. In particular, once you start using multiple models (clones with different constants and TLC configuration), and the 'Trace Explorer' feature to debug specs, you'll probably want to stick to using the IDE. The only time I've needed the command-line tools is to run slave nodes for the distributed model checker.

>>This "Spec Explorer" thing: where does this state live, and why do I have to import things into it?

Have you tried looking in the online help, built into the IDE? It's fairly comprehensive, and very useful.

regards,
Chris

[1] http://research.microsoft.com/en-us/um/people/lamport/tla/summary.pdf Note: the cheat-sheet does not cover extensions in v2 ('TLA+2') of the language, e.g. the LAMBDA keyword.
[2] http://research.microsoft.com/en-us/um/people/lamport/tla/wildfire-challenge.html

[3] This:

B == \/ TRUE
\/ TRUE
=> FALSE (* means (TRUE \/ TRUE) => FALSE, so B = FALSE *)

is very different to this

B == \/ TRUE
\/ TRUE
=> FALSE (* means TRUE \/ (TRUE => FALSE), so B = TRUE *)

I would occasionally type the second, when I intended (the meaning of) the first.

Note that the following means the same as the second statement above, _not_ the first.

B == \/ TRUE
\/ TRUE
=> FALSE (* means TRUE \/ (TRUE => FALSE), so B = TRUE *)

On Wed, Nov 19, 2014 at 3:07 PM, James Fisher <jamesh...@xxxxxxxxx> wrote:

I started to reply to a different thread, but it grew out of
control. I thought I would put down some of my experiences with TLA+
after a short time using it, in the hope that my user feedback is
helpful to goal of attracting new users.

A little about me: I am a professional programmer with an academic
background. I found out about TLA+ via a paper about its use at AWS,
then I watched Leslie's fantastic talk "Thinking for Programmers". I
was quickly attracted to TLA as a simple formalism which might help me
reason about my work in ways that other formalisms have not
particularly helped me. I was attracted to TLA+ for the model checker
and as a way to introduce formal specification into teams of
"practical" programmers (as I see AWS is doing). I work in
environments where even informal specification is unfashionable. I
have currently been reading about and playing with TLA+ for a few days
outside of work.

My first bad experience was visiting (what I thought was) the
"official" website to find that it is broken. I expect a lot of
curious readers would give up right here: it's a signal that the
project is small or dead. TLA+ needs to put the web first and sort out
the tlaplus.net domain. In the mind of the programmer, things without
a dedicated domain name barely qualify as existing. Even the most
obscure software tools have official websites with an element of
community-owned spirit. A domain name builds identity; a
"please-don't-copy-this-UUID" string doesn't.

My second bad experience was attempting to find the documentation. The
website must have HTML hyperlinked documentation. Not hyperlinked PDFs
which I have to download in a zip file and then open with a special
PDF reader. HTML and URLs are king; not PDFs and UUIDs. While I value
typesetting, I value the linkability of the web much more. (I should
emphasize that the *content* of all PDFs I have read has been first
rate: it's all superbly written.)

My third bad experience was with the command-line tools. It took time
and effort to install them: why a jar and a zip? Why do I have to do
some Java-specific stuff to use it; shouldn't their Java
implementation be an implementation detail? It then took time to work
out how to run the programs; I didn't even know how *find out* how to
use them. TLA+ needs to put the command-line tools first: in the
programmer's world, command-line tools are how we interact with our
files. In an ideal world this is how I would interact with TLA+:

> sudo apt-get install tla
> man tla # if this doesn't work, try `tla --help` or just `tla`
> tla repl # play around building a spec
> nano clock.tla # eventually put it in a file
> tla syntax-check clock.tla
> nano clock.tlamodel
> tla model-check clock.tlamodel > results.txt
> git add clock.tla clock.tlamodel
> git commit
> git push
[CI server runs tla model-check and rejects my commit if it finds errors]

TLA+ is not so different from real-world programming languages: we
write (abstract) programs, then we compile/typecheck them, we run
them, we debug them. The workflow for TLA+ should be similar to, say,
Haskell. GHC has a compiler, a REPL, and a few command-line tools. It
does not have an isolated IDE; nor does it need one. Even tools like
Coq or Isabelle, which have their own little IDEs for interactive
proof assistants, are usually used via other generic IDEs like
Emacs.

After reading that the IDE was the recommended way to do things, I
installed it. I had a few bad experiences with it. Outright bugs are
the most obvious but I'll omit those. I found aspects of the IDE
confusing. "Save" to open a file? Okay. This "Spec Explorer" thing:
where does this state live, and why do I have to import things into
it? My *filesystem* should be my spec explorer. It took me a while to
discover those foo.toolbox directories containing my models, encoded
in some semi-human-readable format. I want my models to be
hand-written, first-class citizens that I can put where I want, add to
version control, etc. I want my model-checking results in a standard
format that can be consumed by a CI server, like my unit test results.

In short I think it would be a lot better use of time for TLA+ to
maintain some syntax-highlighting definitions for common editors, and
some idiomatic command-line tools, compared to maintaining a full IDE.

My final significant bad experiences were with reading the "fancy
format" PDFs. Here's what I found myself doing when learning TLA+: (1)
read fancy notation in a paper; (2) attempt to write it out in TLA+
Toolbox; (3) realize I don't know the plaintext notation for
something; (4) find and open Specifying Systems PDF; (5) find the
section in the TOC about syntax; (6) tell my PDF reader to go to that
page number; (7) realize my PDF reader's idea of page numbers is
different to the internal page numbers in the book; (8) scroll around
until I find the definition of the plaintext syntax; (9) scroll around
until I find the symbol that I'm looking for, which might take a
while; (10) type it into TLA+ Toolbox; (11) forgotten what I was doing
in the first place. I'm being picky, maybe; but I found myself getting
seriously annoyed by that workflow when I just wanted to concentrate
on the domain problem. Here's what the workflow would look like if the
tutorials just used the plaintext format: (1) read plaintext notation
in a paper; (2) copy it into TLA+ Toolbox. Sometimes I've found the
fancy format actively confusing. What's the difference between a bold
extential quantifier and a non-bold one? To my programmer mindset,
it's a formatting quirk, not a semantic difference. TLA+ needs to put
plaintext first. In the programmer's world, plaintext is an undisputed
king. We write plaintext, we think plaintext, we store plaintext on
disk, we store plaintext in version control, we copy and paste
plaintext on email/IM, we pipe plaintext from one program to another,
etc etc etc. The power of plaintext means that the fancy math format
for TLA+ will always be in the margins. Programmers don't want to have
to mentally translate between fancy math notation and real-world LaTeX
notation; they want a single plaintext notation. Programmers don't
want to have to compile their work to a PDF in order to read it or
communicate about it. Programmers don't want TLA+ to produce beautiful
books; they want TLA+ to help them _think_. At best, the fancy format
is a minor helpful tool for academics, like similar tools that will
fancy-print Haskell code. At worst, the fancy format is a barrier to
entry which serves to give the (wrong) impression that TLA+ sits in a
dry Platonic mathematical universe that us real-world programmers and
programs don't have easy access to. (Note that I say "plaintext", not
"ASCII". Unicode and UTF-8 are very common nowadays, and having
symbols like "∈" in our programs is okay, if unconventional for
historical reasons.)

Anyway, the above criticism is meant with the greatest of respect. TLA
strikes me as a beautiful mathematical tool; the TLA+ tools I have
found to be less so. Personally, I'm enthusiastic enough to continuing
to rough it out, but I expect a lot of other people would have dropped
off along the way. Also, as someone who works day-to-day with Java and
the web, I might at some point be available to help out with the
project, if others agree with me on the direction it should take.

James

--
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.