Publish a full documentation

[pascutto]

Still to do:

• Finish the mutable queue walk-through
• Finish the union-find walk-through
• Write a landing page
• Polish the language specification section
• Finish the FAQ

[jmid]

Here comes a few impressions from reading the current language specification as a first-time reader:

locations.md
Diving straight into locations + attributes was a bit up-hill after having read getting-started and walkthroughs.
I think it would work better
- to have a general language specification intro or
- to rearrange locations.md to let it start with the familiar part first (preprocessor-syntax) and only afterwards explain how
this is realized using a preprocessor mapping it down to OCaml attributes.

[jmid]

formulae.md
What does ?"? mean?

As a reader I was missing an explanation of these productions (also in the light of our syntax discussion):

   | expr "[" expr "<-" expr "]"
   | expr "[" expr ".." expr "]"
   | expr "[" ".." expr "]"
   | expr "[" expr ".." "]"
   | expr "." "(" expr "<-" expr ")"

[jmid]

type-specifications.md

Regarding mutable types:
I was missing an explanation of why you include both ephemeral and mutable?
My guess: ephemeral marks all models mutable. Perhaps finer control is possible by marking only some models mutable?
Explanation: "We could achieve the same by ..."

Later I found some additional explanation in good-practice.md
Here the description indicates that ephemeral is useful to mark some invisible (non-model) parts mutable.
As a reader I would have liked the explanation be collected in one place (type-specifications.md?) and be illustrated with
an example.

constants-specifications.md - rename to constant-specifications.md ?

[jmid]

function-contracts.md

Regarding caution:
"In the absence of a contract" it is unclear which post-condition that "may not hold".

As a first-time reader it was confusing to read about enabling "the default implicit properties about exceptions, mutability,
non-termination, etc." since these haven't been introduced yet. After having read further down, I see these are introduced later.
Here one could either

• rearrange the page to 'declare before use' or
• add a forward pointer

[jmid]

logical.md

• 'Uninterpreted symbols and Axioms' is incomplete.
  There is an axiom example in 'Logical function contracts' however, so perhaps a first version can be completed by rearranging it.

• I was missing an explanation of variant, e.g.,

  "A variant is a termination measure. It has to have type int, be non-negative, and decrease strictly on each recursive call. "

  (but this is just me guessing...)

[jmid]

Here are a few impressions from reading the union-find walkthrough:

• As I first-time reader I hadn't read the language spec. at this point. I was therefore a bit puzzled that ephemeral was listed but not explained. It is mentioned later in the walkthrough in a Tip. Rereading the beginning now I think explicitly referring to the keyword would have helped me: "We can also add that this universe is mutable by marking it ephemeral: ...". In hinsight, I think this would have helped me better understand the later Tip.

• For make, there's a post-condition to express freshness in the universe of 'a elements: ensures not (Set.mem e (old u.dom))
  However I was surprised that no requirement states anything about the element v or its freshness. Does this mean that

  let elm0 = make 1
  let elm1 = make 1
  let elm2 = make 1

  is valid usage of this API? 🤔

• The Gospel expression old (equivalent u x e \/ equivalent u y e) towards the end surprised me as I had originally just thought of old as a modifier 😮 whereas this seems to indicate that it is more of a "scoping mechanishm" along the lines of let open M in e in OCaml. This just got me thinking:

  • Should old be documented in the language specification? (A quick search just found a single occurrence in a Note in
    function-contracts.md under Data mutability​.
  • Should old be added as a Gospel keyword in lexical-conventions.md - or is it a special variable that can it be shadowed by other variables? It would be nice to clarify this in the language spec 🙂