Description
We have received very detailed feedback from @pdini! Many thanks, Paolo!
Quint Tutorial Feedback
Disclaimer: since I am not a computer scientist by training, some of the points below may just be due to my ignorance. However, depending on how wide a net you want to cast to catch users, I might be a useful limiting case 🙂
Classic Markdown
-
Step-by-step explanation is effective and easy to read
-
Tiny English deviations from norm, I would be happy to highlight/fix them for you (they can be distracting)
-
Interesting that the output is stored in a state variable
-
At step 5 the definition or logical = and the assignment = appear to use the same symbol (=). I prefer to use different symbols, for example “=” and “=:“, or “==” and “=”, etc. Since Quint is a front-end for TLA+, maybe these are all logical equals, but I am a bit lost nonetheless because the tutorial talks about assignments. At the same time, you say that these statements should evaluate to True. This is a familiar concept from TLA+, but it does suggest that “=” then is a logical =. I can’t reconcile these different interpretations.
-
Explanation of parallel execution is clear
-
At step 6 there appears to be a typo with the “==” sign for consoleOutput. Since this happens twice, perhaps it is not a typo, in which case it is even more confusing. If “==” means assignment and if there are no typos in step 5, then I don’t understand how you can talk about assignment at step 5. If “==” is a logical equal (so the statement is an enabling condition), then I understand the syntax of step 6, although I don’t understand why it is important for the previous state to be the empty string if in the next state it will be overwritten anyway.
-
Commas at the end of sentences: I don’t understand why in some cases the comma is present for all statements, including the last one in a block, and in other cases it is not present. Example: in Step 7 it is present, in step 8 it is not.
-
“step” appears to be analogous to “next” in TLA+
CodeTour
Very nice animation. It did not add much to the experience for me, however. I am just as happy with the md version.
High-Level Remarks
Although learning through code examples is certainly effective, perhaps some general tips about the language at the beginning of the tutorial would help. In other words, setting the context is probably a good idea. For example, I happen to know that Quint is a syntax front-end for TLA+. A user who does not know that might be rather more confused. At the same time, I have zero experience creating a new language, so I could be totally wrong. In any case, understanding how Quint and TLA+ are related both mathematically and at runtime seems extremely interesting — another kind of tutorial of course!