--I started to reply to a different thread, but it grew out ofcontrol. 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 ishelpful to goal of attracting new users.A little about me: I am a professional programmer with an academicbackground. I found out about TLA+ via a paper about its use at AWS,then I watched Leslie's fantastic talk "Thinking for Programmers". Iwas quickly attracted to TLA as a simple formalism which might help mereason about my work in ways that other formalisms have notparticularly helped me. I was attracted to TLA+ for the model checkerand as a way to introduce formal specification into teams of"practical" programmers (as I see AWS is doing). I work inenvironments where even informal specification is unfashionable. Ihave currently been reading about and playing with TLA+ for a few daysoutside 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 ofcurious readers would give up right here: it's a signal that theproject is small or dead. TLA+ needs to put the web first and sort outthe tlaplus.net domain. In the mind of the programmer, things withouta dedicated domain name barely qualify as existing. Even the mostobscure software tools have official websites with an element ofcommunity-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. Thewebsite must have HTML hyperlinked documentation. Not hyperlinked PDFswhich I have to download in a zip file and then open with a specialPDF reader. HTML and URLs are king; not PDFs and UUIDs. While I valuetypesetting, I value the linkability of the web much more. (I shouldemphasize that the *content* of all PDFs I have read has been firstrate: it's all superbly written.)My third bad experience was with the command-line tools. It took timeand effort to install them: why a jar and a zip? Why do I have to dosome Java-specific stuff to use it; shouldn't their Javaimplementation be an implementation detail? It then took time to workout how to run the programs; I didn't even know how *find out* how touse them. TLA+ needs to put the command-line tools first: in theprogrammer's world, command-line tools are how we interact with ourfiles. 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: wewrite (abstract) programs, then we compile/typecheck them, we runthem, 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. Itdoes not have an isolated IDE; nor does it need one. Even tools likeCoq or Isabelle, which have their own little IDEs for interactiveproof assistants, are usually used via other generic IDEs likeEmacs.After reading that the IDE was the recommended way to do things, Iinstalled it. I had a few bad experiences with it. Outright bugs arethe most obvious but I'll omit those. I found aspects of the IDEconfusing. "Save" to open a file? Okay. This "Spec Explorer" thing:where does this state live, and why do I have to import things intoit? My *filesystem* should be my spec explorer. It took me a while todiscover those foo.toolbox directories containing my models, encodedin some semi-human-readable format. I want my models to behand-written, first-class citizens that I can put where I want, add toversion control, etc. I want my model-checking results in a standardformat 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+ tomaintain some syntax-highlighting definitions for common editors, andsome idiomatic command-line tools, compared to maintaining a full IDE.My final significant bad experiences were with reading the "fancyformat" 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 forsomething; (4) find and open Specifying Systems PDF; (5) find thesection in the TOC about syntax; (6) tell my PDF reader to go to thatpage number; (7) realize my PDF reader's idea of page numbers isdifferent to the internal page numbers in the book; (8) scroll arounduntil I find the definition of the plaintext syntax; (9) scroll arounduntil I find the symbol that I'm looking for, which might take awhile; (10) type it into TLA+ Toolbox; (11) forgotten what I was doingin the first place. I'm being picky, maybe; but I found myself gettingseriously annoyed by that workflow when I just wanted to concentrateon the domain problem. Here's what the workflow would look like if thetutorials just used the plaintext format: (1) read plaintext notationin a paper; (2) copy it into TLA+ Toolbox. Sometimes I've found thefancy format actively confusing. What's the difference between a boldextential quantifier and a non-bold one? To my programmer mindset,it's a formatting quirk, not a semantic difference. TLA+ needs to putplaintext first. In the programmer's world, plaintext is an undisputedking. We write plaintext, we think plaintext, we store plaintext ondisk, we store plaintext in version control, we copy and pasteplaintext on email/IM, we pipe plaintext from one program to another,etc etc etc. The power of plaintext means that the fancy math formatfor TLA+ will always be in the margins. Programmers don't want to haveto mentally translate between fancy math notation and real-world LaTeXnotation; they want a single plaintext notation. Programmers don'twant to have to compile their work to a PDF in order to read it orcommunicate about it. Programmers don't want TLA+ to produce beautifulbooks; they want TLA+ to help them _think_. At best, the fancy formatis a minor helpful tool for academics, like similar tools that willfancy-print Haskell code. At worst, the fancy format is a barrier toentry which serves to give the (wrong) impression that TLA+ sits in adry Platonic mathematical universe that us real-world programmers andprograms don't have easy access to. (Note that I say "plaintext", not"ASCII". Unicode and UTF-8 are very common nowadays, and havingsymbols like "∈" in our programs is okay, if unconventional forhistorical reasons.)Anyway, the above criticism is meant with the greatest of respect. TLAstrikes me as a beautiful mathematical tool; the TLA+ tools I havefound to be less so. Personally, I'm enthusiastic enough to continuingto rough it out, but I expect a lot of other people would have droppedoff along the way. Also, as someone who works day-to-day with Java andthe web, I might at some point be available to help out with theproject, 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.