glossary feedback

Author: RalfJung

reference/src/glossary.md

@@ -76,9 +76,9 @@ niche.
 #### Place
 
 A *place* (called "lvalue" in C and "glvalue" in C++) is the result of computing a [*place expression*][place-value-expr].
-A place definitely stores some location in memory (a "pointer"), and might contain more information such as size or alignment (the details will have to be determined as the Rust Abstract Machine gets specified more precisely).
+A place is basically a pointer (pointing to some location in memory, potentially carrying [provenance](#pointer-provenance)), but might contain more information such as size or alignment (the details will have to be determined as the Rust Abstract Machine gets specified more precisely).
 A place has a type.
-Places are ephemeral; they arise during the computation of an instruction but cannot be persisted in memory.
+Places cannot be "stored" in memory, only [values](#value) can.
 
 The key operations on a place are:
 * storing a [value](#value) of the same type in it (when it is used on the left-hand side of an assignment),
@@ -89,21 +89,21 @@ The key operations on a place are:
 #### Value
 
 A *value* (called "value of the expression" or "rvalue" in C and "prvalue" in C++) is what gets stored in a [place](#place), and also the result of computing a [*value expression*][place-value-expr].
-A value has a type.
+A value has a type, and it denotes the abstract mathematical concept that is represented by data in our programs.
 For example, a value of type `u8` is a mathematical integer in the range `0..256`.
 Values can be (according to their type) turned into a list of bytes, which is called a [representation](#representation) of the value.
 Values are ephemeral; they arise during the computation of an instruction but are only ever persisted in memory through their representation.
+(This is comparable to how run-time data in a program is ephemeral and is only ever persisted in serialized form.)
 
 #### Representation (relation)
 
 A *representation* of a [value](#value) is a list of bytes that is used to store or "represent" that value in memory.
 
 We also sometimes speak of the *representation of a type*; this should more correctly be called the *representation relation* as it relates values of this type to lists of bytes that represent this value.
-The term "relation" here is used in the mathematical sense, i.e. the representation relation is a set of pairs of values and lists of bytes.
-You can also think of it as a predicate that, given a value and a list of bytes, says whether this value is represented by that list of bytes.
+The term "relation" here is used in the mathematical sense: the representation relation is a predicate that, given a value and a list of bytes, says whether this value is represented by that list of bytes (`val -> list byte -> Prop`).
 
 The relation should be functional for a fixed list of bytes (i.e., every list of bytes has at most one associated representation).
-It is partial in both directions: not all values have a representation (e.g. the mathematical integer `300` has no representation at type `u8`), and not all lists of bytes correspond to a value of some type (e.g. lists of the wrong size correspond to no value, and the list consisting of the single byte `0x10` corresponds to no value of type `bool`).
+It is partial in both directions: not all values have a representation (e.g. the mathematical integer `300` has no representation at type `u8`), and not all lists of bytes correspond to a value of a specific type (e.g. lists of the wrong size correspond to no value, and the list consisting of the single byte `0x10` corresponds to no value of type `bool`).
 For a fixed value, there can be many representations (e.g., when considering type `#[repr(C)] Pair(u8, u16)`, the second byte is a padding byte so changing it does not affect the value represented by a list of bytes).
 
 See the [value domain][value-domain] for an example how values and representation relations can be made more precise.