3 ms·

It's still a barrier for beginners. I teach both TLA+ and Alloy and people struggle with remembering TLA+ tokens much more than they do with Alloy, which has sy

by hwayne 6y ago

It's still a barrier for beginners. I teach both TLA+ and Alloy and people struggle with remembering TLA+ tokens much more than they do with Alloy, which has synonyms for common operators. You can write `implies` instead of `=>` if you want, which makes the teaching experience much smoother. If I could have students use `&&`, `||`, and `!` instead of ⋀ ⋁ ¬ that'd cut out a lot of early friction. This is also why I "pythonize" the TLA+ tokens during talks. Trying to explain the math syntax gets in the way of explaining the core ideas.

pron 6y ago
I agree it's a barrier for beginners, but I think this is a good barrier, which makes the next, bigger ones, easier to overcome. A step is also a barrier, but I'd rather face more, lower steps than fewer taller ones. By the time you realise neither operators nor functions work at all like functions from programming, the syntax has helped to put your mind in a "this is not programming" mode. Also, || and && are almost universally used in programming languages today, but they weren't thirty years ago, and might not be thirty years from now (Zig doesn't use them and neither does Nim), and even in C, C++, and Rust they have similar but subtly different meaning than | and & involving evaluation, a concept that TLA+ doesn't have -- now there's a more interesting and more important unfamiliar TLA+ thing -- while ∨ and ∧ have been used much longer than that and aren't going anywhere. So every person might prefer something that's already familiar to them, but there is no alternative that's really universal. If you go to Wikipedia -- say, https://en.wikipedia.org/wiki/Logical_connective https://en.wikipedia.org/wiki/Logical_connective -- they use "TLA+ notation," not C notation. Anyway, there are other, and more important, things in TLA+ that are much less familiar from programming (e.g. there's no evaluation) than how to write logical or, and still TLA+ has been more successful at teaching programmers to specify more complex systems more quickly than any other specification language I'm aware of.

by hwayne 6y ago

pron 6y ago

I agree it's a barrier for beginners, but I think this is a good barrier, which makes the next, bigger ones, easier to overcome. A step is also a barrier, but I'd rather face more, lower steps than fewer taller ones. By the time you realise neither operators nor functions work at all like functions from programming, the syntax has helped to put your mind in a "this is not programming" mode. Also, || and && are almost universally used in programming languages today, but they weren't thirty years ago, and might not be thirty years from now (Zig doesn't use them and neither does Nim), and even in C, C++, and Rust they have similar but subtly different meaning than | and & involving evaluation, a concept that TLA+ doesn't have -- now there's a more interesting and more important unfamiliar TLA+ thing -- while ∨ and ∧ have been used much longer than that and aren't going anywhere. So every person might prefer something that's already familiar to them, but there is no alternative that's really universal. If you go to Wikipedia -- say, https://en.wikipedia.org/wiki/Logical_connective https://en.wikipedia.org/wiki/Logical_connective -- they use "TLA+ notation," not C notation. Anyway, there are other, and more important, things in TLA+ that are much less familiar from programming (e.g. there's no evaluation) than how to write logical or, and still TLA+ has been more successful at teaching programmers to specify more complex systems more quickly than any other specification language I'm aware of.