3 ms·

Nah, I just honestly very much dislike the choices about syntax. Like why on earth would you make rules like "some number of repeated punctuation on a separate

Nah, I just honestly very much dislike the choices about syntax. 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). 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.

pron 3y ago
> 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-long-formula/ 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 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/Maths1.pdf - https://pron.github.io/files/SelfRefPuzzle.pdf https://pron.github.io/files/SelfRefPuzzle.pdf, - https://pron.github.io/files/TicTacToe.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.

pron 3y ago

> 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-long-formula/ 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 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/Maths1.pdf - https://pron.github.io/files/SelfRefPuzzle.pdf https://pron.github.io/files/SelfRefPuzzle.pdf, - https://pron.github.io/files/TicTacToe.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.