I understand his logic, but at the same time, TLA+'s weird surface syntax put off a lot of people who otherwise could have used it. And PlusCal seemed like a halfway measure: more like a programming language, but still kinda... weird.
So, I welcome Quint. And it's great that they seem interested in making the tooling fit with the normal developer ecosystem, such as LSP support.
We still have lots of ways to improve, and -- we think -- lots of opportunities to improve our interop and complementary qualities in relation to TLA+ and TLC. But we have found the tools in their current state useful enough to be worth sharing :)
The simple mathematical syntax (and semantics [1]) of TLA+ has the advantage of making mathematical reasoning easier and it's more expressive; if it were like a programming language there would be too many things that TLA+ users would want to do but couldn't, certainly not as easily. Programming-language-like syntax and semantics has the advantage of being more familiar to programmers (many of which just want to run a model checker, and aren't interested in a more mathematical analysis of the specification (which actually makes specification easier, but only after gaining some experience). The two kinds of languages make different kinds of things either easier or harder.
Overall, being programming-like helps programmers who just want model checking and then maybe to start dipping their toes into specification.
----
[1]: What's more challenging for programmers is less the syntax and more the semantics. For example, the following function definition in TLA+ (using ASCII syntax) happens to look a lot like programming in this particular case:
f[x \in Int] == -f[x]
Another example could be (again, using the ASCII syntax):
Inc(x) == x + 1
3 = Inc(x)'
Those who aren't interested may still benefit from languages that are programming-like and offer model-checking. That's great, too!
There is no need for such ambiguity. It makes parsing harder. It makes it hard to recognize that it's actually an element with some semantics attached and not just a weird decoration.
Also, a lot of capitalization.
TLA+ programs, from typographic perspective, look really, really awful.
There are languages which just look bad due to weird typographical choices of their authors. Usually because they use symbols in the context the font author never expected them to be used. For example, any language that uses camel-case or pascal-case is an affront to typography because font authors don't anticipate capital letters in the middle of the word surrounded by minuscule letters. Similarly, nobody expects sequences of "=" signs or ":" written adjacent to the following word rather than previous one etc.
Some look really awful due to extreme abuse of punctuation (C++ would be a good example with all the &&::<<<*_>>,<**>> stuff), others look very repetitive to the point that they make you lose focus (eg. Pascal-style language which have "if-then-else-end if" going on where sometimes for many lines you just keep reading the "cargo train" of "end, end, end, end if, end". Lisps are also in this category because they usually look too uniform.
TLA+ looks like a Fortran program from the 60's formatted on a physical typewriter with all sorts of weird uses of the small number of available glyphs to substitute for the actual typographical thing that wasn't available to the author.
That's not how it works, and Lamport has done a lot of exploration and explains it in detail in How to Write a Long Formula (1994): https://www.microsoft.com/en-us/research/publication/write-l... Writing it long hand, i.e. without TLA+'s special contribution to mathematical syntax, would mean a lot of parentheses that would be much harder to parse. From the conclusion: "The notations introduced here will be unfamiliar to most readers, and unfamiliar notation usually seems unnatural. I have used the notations for several years, and I now find them indispensable. I urge the reader to rewrite formula I of Figure 1 in conventional notation and compare it with the original. Having to keep track of six or seven levels of parentheses reveals the advantage of using indentation to eliminate parentheses."
But, if you prefer, you can use parentheses and dispense with indented lists altogether. The language supports that just fine. In other words, Lamport claims that indentation is clearer than brackets, but he doesn't force that on you in TLA+. You find brackets clearer? No problem! TLA+ allows you to use indentation in lieu of brackets if, like Lamport, you think it makes complex formulas easier to read, but it doesn't force you. However, you should know that a lot of thought has gone into that syntax (by a a Turing award laureate), probably more thought than has gone into most other formal languages' syntax, and at the very least you may want to reserve judgment for a while.
TLA+ syntax is pretty much the standard mathematical and logical syntax, as it has evolved primarily since Peano over about a hundred years, with just a few modifications by Lamport to make it more regular and less ambiguous and more suited to writing the larger formulas needed to describe engineered systems as opposed to natural systems.
> TLA+ programs, from typographic perspective, look really, really awful.
There are no programs you write in TLA+, only mathematical formulas, and they look pretty much exactly like all mathematics does on the page. You can see lots of examples on this chapter of my blog post series on TLA+: https://pron.github.io/posts/tlaplus_part2. TLA+ looks pretty close to anything you'd find in formal logic book.
Here are a couple more examples:
- https://pron.github.io/files/Maths1.pdf
- https://pron.github.io/files/SelfRefPuzzle.pdf,
- https://pron.github.io/files/TicTacToe.pdf (the entire post is written in TLA+)
Maybe it's just me, but I find that syntax quite pretty, and very familiar.
> TLA+ looks like a Fortran program from the 60's
Oh, I think you're not talking about the actual TLA+ syntax, but it's typesetting source (which works like LaTeX source). Actual TLA+ syntax is read in pretty-printed form.
Given that LaTeX is how we normally write mathematics on a computer, TLA+ is a marked improvement (I had to write that post I linked in LaTeX and it was much less pleasant than the TLA+ typesetting source). Honestly, I can't think of any other language for writing mathematics that has a cleaner, prettier syntax than TLA+ (Lean is not terrible, but it's further removed from the standard mathematical notation), but if you know of one, let me know.