> Like why on earth would you make rules like "some number of repeated punctuation on a separate line means something" (I hate this about Markdown too).

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.