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