search

hwayne / learntla-v2

Learn TLA+ for free! No prior experience necessary!
https://www.learntla.com
Other
183 stars 39 forks source link

Vocabulary #80

Open keithb-coop opened 3 months ago

keithb-coop commented 3 months ago

It's bewildering to me that the first example specification in the body text contains only a thing called an algorithm, which moreover doesn't seem to do anything meaningful. I understand that it's just a syntactically valid lump to use to point at to name some parts but my autistic brain gets stopped at this point. It's…an algorithm, says so right there, algorithm and it talks about changing some variables. So what does it specify, if it's a specification?

hwayne commented 3 months ago

Technically it's a specification of an algorithm, in the broad sense of the word "algorithm". Are you asking me to define a specification more clearly?

keithb-coop commented 3 months ago

Two things about the example confuse me:

  1. as someone with a background in Z-style specification, its confusing to me that this "specification" says only what to do and not how to know that it was done correctly.
  2. there doesn't seem to be a "correctly", it's just stuff

So, I'd ask for a clearer explanation (not definition) of why the first thing in a specification is an algorithm and for the first example algorithm specification to be meaningful. Doesn't have to be complex or clever, but it would be nice if it didn't prompt me to spend several minutes wondering if I've missed the point somehow and it's meant to be meaningful.