diff --git a/doc/ref/spec.md b/doc/ref/spec.md
index 4faa44c..8d4cecb 100644
--- a/doc/ref/spec.md
+++ b/doc/ref/spec.md
@@ -227,7 +227,7 @@
 
 #### Preamble
 
-The following pseudo-keywords are used at the preamble of a CUE file.
+The following keywords are used at the preamble of a CUE file.
 After the preamble, they may be used as identifiers to refer to namesake fields.
 
 ```
@@ -237,13 +237,13 @@
 
 #### Comprehension clauses
 
-The following pseudo-keywords are used in comprehensions.
+The following keywords are used in comprehensions.
 
 ```
 for          in           if           let
 ```
 
-The pseudo-keywords `for`, `if` and `let` cannot be used as identifiers to
+The keywords `for`, `if` and `let` cannot be used as identifiers to
 refer to fields. All others can.
 
 <!--
@@ -346,6 +346,7 @@
 
 
 ### String and byte sequence literals
+
 A string literal represents a string constant obtained from concatenating a
 sequence of characters.
 Byte sequences are a sequence of bytes.
@@ -581,7 +582,7 @@
 ### Unification
 
 The _unification_ of values `a` and `b`, denoted as `a & b` in CUE,
-is defined as the greatest lower bound of `a` and `b`. (That is, the 
+is defined as the greatest lower bound of `a` and `b`. (That is, the
 value `u` such that `u ⊑ a` and `u ⊑ b`,
 and for any other value `v` for which `v ⊑ a` and `v ⊑ b`
 it holds that `v ⊑ u`.)
@@ -595,130 +596,120 @@
 on top of it.
 
 Syntactically, unification is a [binary expression](#Operands).
-
+<!-- TODO: explicitly mention that disjunction is not a binary operation
+but a definition of a single value?-->
 
 ### Disjunction
 
 A _disjunction_ of two values `a` and `b`, denoted as `a | b` in CUE,
-is defined as the smallest value `d` such that `a ⊑ d` and `b ⊑ d`.
+defines the smallest value `d` such that `a ⊑ d` and `b ⊑ d`.
+This style of disjunctions is sometimes also referred to as sum types.
+
 These all follow from the definition of disjunction:
 - The disjunction of `a` with itself is always `a`.
 - The disjunction of a value `a` and `b` where `a ⊑ b` is always `b`.
 - The disjunction of a value `a` with bottom is always `a`.
 - The disjunction of two bottom values is bottom.
 
+Elements that evaluate to bottom are eliminated from a disjunction.
+A disjunction evaluates to bottom (`_|_`) if it has no elements
+after such elimination.
+
 Syntactically, disjunction is a [binary expression](#Operands).
 
-Implementations should report an error if for a disjunction `a | ... | b`
-where `b` is an instance of `a`, as `b` will be superfluous and can never
-be selected as a default. <!-- jba: either put this paragraph later, or link 
-to the discussion of defaults. -->
-
-If a disjunction is used in any operation other than unification or another
-disjunction, the default value is chosen before operating on it.
-<!-- jba: I wish that the default mechanism wasn't so intertwined with
-     disjunction. Like Prolog "cut," it breaks the beautiful functional
-     structure. 
-     
-     But reading the Kubernetes examples, I see how pervasive and useful it is.
--->
-
-   
+The unification of a disjunction with another value is equal to the disjunction
+composed of the unification of this value with all of the original elements
+of the disjunction.
+In other words, unification distributes over disjunction.
+So
 
 ```
-Expression                Result (without picking default)
+(a_0 | ... |a_n) & b ==> a_0&b | ... | a_n&b,
+```
+
+with values evaluating to bottom removed from the resulting disjunction.
+
+```
+Expression                Result
+({a:1} | {b:2}) & {c:3}   {a:1, c:3} | {b:2, c:3}
 (int | string) & "foo"    "foo"
 ("a" | "b") & "c"         _|_
-
-(3 | 5) + 2               5
 ```
 
-If the values of a disjunction are unambiguous, its first value may be taken
-as a default value. <!-- jba: move this sentence higher -->
+Unification of two disjunctions is defined to retain a strict ordering
+of the elements of the resulting disjunction:
 
-The default value for a disjunction is selected when:
-
-1. passing it to an argument of a call or index value,
-1. using it in any unary or binary expression except for unification or disjunction,
-1. using it as the receiver of a call, index, slice, or selector expression, and
-1. a value is taken for a configuration. <!-- jba: not clear what this phrase means -->
-<!-- jba: you said this above more concisely as "anything other than unification
-or disjunction". -->
-
-<!-- jba: This rule concerns me. It seems to imply that the default value can be
-used even if it is not ultimately selected as the concrete value for the
-disjunction. Example:
-
-    a: 1 | int
-    b: a+1
-    // later
-    a: 2
-
-You say "the default value for a disjunction is selected when...using it in any
-unary or binary expression except for unification or disjunction", so 1 is
-selected for `a` in the second line, and therefore `b` is 2. But then `a` is 2,
-so the constraint on the second line is violated at the end of the evaluation.
-
-Maybe the rule only applies to disjunction expressions that appear as part of
-other expressions, not when they are the value of a field? 
+```
+(a_0 | ... | a_n) & (b_0 | ... | b_m) =>
+a_0&b_0 | ... | a_n&b_0 | a_0&b_1 | ... | a_n&b_m
+```
+<!-- Note that there are several variants of ordering that would work here.
+It only matters that there exists a pre-determined order.
 -->
 
-<!-- jba
-Assuming I'm right about the above and the default is not always selected in expressions,
-then it can matter which order the defaults are selected. Consider:
+The _first value_ of a disjunction is the first element in a disjunction
+after eliminating values evaluating to bottom.
+The ordering is irrelevant for the placement of a disjunction within the
+lattice of values, but it is relevant for default values, which we will
+discuss next.
 
-    a: 1 | int
-    b: 2 | int
-    c: a + b
-    c: 4
+#### Default values
 
-After applying all constraints, I don't have concrete values for `a` or `b`, so
-I must select a default and then re-run my constraint engine. (At least that's
-how I imagine the implementation to work.) 
+A disjunction evaluates to its _default_ value if it is used as a value for any
+operation other than unification or disjunction.
+The default value of a disjunction is its first value or
+bottom in case of a manifest failure.
+A _manifest failure_ occurs if
+the disjunction resulted from the unification of two or more disjunctions and
+these disjunctions can be unified in different orders such that they
+result in different first values.
 
-If I select `a` first, then I end with a==1 and b=3. If I select `b` first, then
-I get b==2 and a==2.
+<!-- TODO(mpvl): consider it to be a manifest failure if if non-concrete
+values are used in expressions requiring concrete values.
 -->
 
-
-A value is unambiguous if a disjunction has never been unified with another
-disjunction, or if the first element is the result of unifying two first
-values of a disjunction.
-<!-- jba: Hard to understand this sentence, or why a disjunction must be
-unambiguous to use its first value as a default. -->
+A default value is chosen if the disjunction is not used
+in a unification or disjunction operation.
+This means that in practice, a default is chosen for almost any expression
+that does not involve `&` and `|`, including slices, indices, selectors,
+and all but a few explicitly marked builtin functions.
 
 ```
 Expression                       Default
-("tcp"|"udp") & ("tcp"|"udp")    "tcp"  // default chosen
-("tcp"|"udp") & ("udp"|"tcp")    _|_    // no unique default
+"tcp" | "udp"                    "tcp"
+1 | int                          1
+string | 1.0                     string
 
-("a"|"b") & ("b"|"a") & "a"      "a"    // single value after evaluation
+("tcp"|"udp") & ("tcp"|"udp")    "tcp"
+("tcp"|"udp") & ("udp"|"tcp")    _|_ // ambiguous: no unique first value
 ```
-<!-- jba: the first two examples here contradict your assertion that -->
-<!-- defaults are not chosen under unfication and disjunction. Both should have -->
-<!-- the result ("tcp"|"udp"). -->
 
+A disjunction always evaluates to the same default value, regardless of
+the context in which the value is used.
+For instance, `[1, 3]["a" | 1]` will result in an error, as `"a"` will be
+selected as the default value.
+
+
+```
+[1, 2]["a" | 1]          //  _|_ // "a" is not an integer value
+[1, 2][("a" | 1) & int]  //  2
+```
+
+Implementations should report an error for a disjunction `a | ... | b`,
+where `b` is an instance of `a`, as `b` will be superfluous and can never
+be selected as a default.
 
 
 ### Bottom and errors
 
 Any evaluation error in CUE results in a bottom value, respresented by
 the token '_|_'.
-Bottom is an instance of every other prototype.
+Bottom is an instance of every other value.
 Any evaluation error is represented as bottom.
 
 Implementations may associate error strings with different instances of bottom;
 logically they all remain the same value.
 
-```
-Expr         Result
- 1  &  2       _|_
-int & bool     _|_
-_|_ |  1        1
-_|_ &  2       _|_
-_|_ & _|_      _|_
-```
-
 
 ### Top
 
@@ -736,9 +727,9 @@
 
 ### Null
 
-The _null value_ is represented with the pseudo-keyword `null`.
+The _null value_ is represented with the keyword `null`.
 It has only one parent, top, and one child, bottom.
-It is unordered with respect to any other prototype.
+It is unordered with respect to any other value.
 
 ```
 null_lit   = "null"
@@ -754,7 +745,7 @@
 ### Boolean values
 
 A _boolean type_ represents the set of Boolean truth values denoted by
-the pseudo-keywords `true` and `false`.
+the keywords `true` and `false`.
 The predeclared boolean type is `bool`; it is a defined type and a separate
 element in the lattice.
 
@@ -862,6 +853,7 @@
 
 We say a label is defined for a struct if the struct has a field with the
 corresponding label.
+The value for a label `f` of struct `a` is denoted `f.a`.
 A struct `a` is an instance of `b`, or `a ⊑ b`, if for any label `f`
 defined for `b`, label `f` is also defined for `a` and `a.f ⊑ b.f`.
 Note that if `a` is an instance of `b` it may have fields with labels that
@@ -870,12 +862,14 @@
 The (unique) struct with no fields, written `{}`, has every struct as an
 instance. It can be considered the type of all structs.
 
-The unification of structs `a` and `b` is a new struct `c` which
+The successful unification of structs `a` and `b` is a new struct `c` which
 has all fields of both `a` and `b`, where
 the value of a field `f` in `c` is `a.f & b.f` if `f` is in both `a` and `b`,
 or just `a.f` or `b.f` if `f` is in just `a` or `b`, respectively.
 Any [references](#References) to `a` or `b`
 in their respective field values need to be replaced with references to `c`.
+The result of a unification is bottom (`_|_`) if any of its fields evaluates
+to bottom, recursively.
 
 A field name may also be an interpolated string.
 Identifiers used in such strings are evaluated within
@@ -966,10 +960,10 @@
 
 ### Lists
 
-A list literal defines a new prototype of type list.
+A list literal defines a new value of type list.
 A list may be open or closed.
 An open list is indicated with a `...` at the end of an element list,
-optionally followed by a prototype for the remaining elements.
+optionally followed by a value for the remaining elements.
 
 The length of a closed list is the number of elements it contains.
 The length of an open list is the its number of elements as a lower bound
@@ -1307,8 +1301,8 @@
 ```
 constructs a substring or slice. The indices `low` and `high` must be
 concrete integers and select
-which elements of operand a appear in the result. The result has indices
-starting at 0 and length equal to `high` - `low`.
+which elements of operand `a` appear in the result.
+The result has indices starting at 0 and length equal to `high` - `low`.
 After slicing the list `a`
 <!-- TODO(jba): how does slicing open lists work? -->
 
@@ -1366,14 +1360,16 @@
 ```
 <!-- TODO: consider adding unary_op: "<" | "<=" | ">" | ">=" -->
 
-Comparisons are discussed [elsewhere]. For other binary operators, the operand
-types must be [identical] unless the operation involves untyped [constants]
-or durations. For operations involving constants only, see the section on
-[constant expressions].
+Comparisons are discussed [elsewhere](#Comparison-operators).
+For other binary operators, the operand
+types must unify.
+<!-- TODO: durations
+ unless the operation involves durations.
 
 Except for duration operations, if one operand is an untyped [literal] and the
 other operand is not, the constant is [converted] to the type of the other
 operand.
+-->
 
 
 #### Operator precedence
@@ -1486,6 +1482,7 @@
 For decimal floating-point numbers, `+x` is the same as `x`,
 while -x is the negation of x.
 The result of a floating-point division by zero is bottom (an error).
+<!-- TODO: consider making it +/- Inf -->
 
 An implementation may combine multiple floating-point operations into a single
 fused operation, possibly across statements, and produce a result that differs
@@ -1495,7 +1492,7 @@
 #### List operators
 
 Lists can be concatenated using the `+` operator.
-For lists `a` and `b`, 
+For lists `a` and `b`,
 ```
 a + b
 ```
@@ -1541,7 +1538,7 @@
 }
 
 rangeList:  (1..2)*[int]
-rangeListT: null | {
+rangeListT: {
     Elem: int
     Tail: {
         Elem: int
@@ -1561,8 +1558,8 @@
     }
 }
 ```
-<!-- jba: I thought (1..2)*[int] is equivalent to [int] | [int, int]
-     but rangeListT is not that. -->
+<!-- TODO(mpvl): should we disallow multiplication with a range?
+If so, how does one specify a list with a range of possible lengths? -->
 
 <!-- jba: Clarify the allowed values for the non-list operand. And must that be 
 the left operand? -->
@@ -1694,40 +1691,10 @@
 `x'` is an instance of `T`.
 A value `x` can be converted to the type of `T` in any of these cases:
 
-- `x` is of type struct and is subsumed by `T` ignoring struct tags.
-- `x` and `T` are both integer or floating point types.
-- `x` is an integer or a list of bytes or runes and `T` is a string type.
-<!-- jba: first mention of runes -->
-- `x` is a string and `T` is a list of bytes or runes.
-
-
-<!--
-[Field tags] are ignored when comparing struct types for identity
-for the purpose of conversion:
-
-```
-person: {
-    name:    string #xml:"Name"
-    address: null | {
-        street: string #xml:"Street"
-        city:   string #xml:"City"
-    }  #xml:"Address"
-}
-
-person2: {
-    name:    string
-    address: null | {
-        street: string
-        city:   string
-    }
-}
-
-p2 = person(person2)  // ignoring tags, the underlying types are identical
-```
--->
-
-<!-- jba: I don't know what the type of a struct is, other than {}. -->
-
+- `x` is a struct and is subsumed by `T`.
+- `x` and `T` are both integer or floating points.
+- `x` is an integer or a byte sequence and `T` is a string.
+- `x` is a string and `T` is a byte sequence.
 
 Specific rules apply to conversions between numeric types, structs,
 or to and from a string type. These conversions may change the representation
@@ -1738,7 +1705,7 @@
 #### Conversions between numeric ranges
 For the conversion of numeric values, the following rules apply:
 
-1. Any integer prototype can be converted into any other integer prototype
+1. Any integer value can be converted into any other integer value
    provided that it is within range.
 2. When converting a decimal floating-point number to an integer, the fraction
    is discarded (truncation towards zero). TODO: or disallow truncating?
@@ -1774,7 +1741,6 @@
 Conversions between list types are possible only if `T` strictly subsumes `x`
 and the result will be the unification of `T` and `x`.
 
-<!---
 If we introduce named types this would be different from IP & [10, ...]
 
 Consider removing this until it has a different meaning.
@@ -1922,14 +1888,19 @@
 Argument type    Result
 
 string            string length in bytes
-list              list length
+bytes             length of byte sequence
+list              list length, smallest length for an open list
 struct            number of distinct fields
 ```
-<!-- jba: 
-   String length contradicts what you said in the Strings section near the beginning.
-   What does len([1, 2, ...]) return?
-   If [1] is actually { Elem: 1, Tail: null}, then wouldn't len([1]) == 2?
--->
+
+```
+Expression           Result
+len("Hellø")         6
+len([1, 2, 3])       3
+len([1, 2, ...])     2
+len({a:1, b:2})      2
+```
+
 
 ### `required`
 
@@ -2095,16 +2066,16 @@
 A CUE configuration can be defined in terms of constraints, which are
 analogous to typed attribute structures referred to above.
 
-#### Definition of basic prototypes
+#### Definition of basic values
 
-> A _basic prototype_ is any CUE prototype that is not a struct (or, by
+> A _basic value_ is any CUE value that is not a struct (or, by
 > extension, a list).
-> All basic prototypes are partially ordered in a lattice, such that for any
-> basic prototype `a` and `b` there is a unique greatest lower bound
+> All basic values are partially ordered in a lattice, such that for any
+> basic value `a` and `b` there is a unique greatest lower bound
 > defined for the subsumption relation `a ⊑ b`.
 
 ```
-Basic prototypes
+Basic values
 null
 true
 bool
@@ -2116,7 +2087,7 @@
 re("Hello .*!")
 ```
 
-The basic prototypes correspond to their respective types defined earlier.
+The basic values correspond to their respective types defined earlier.
 
 Struct (and by extension lists), are represented by the abstract notion of
 a typed feature structure.
@@ -2161,11 +2132,11 @@
 >
 > The set of _terms_ for label set `Label` is recursively defined as
 >
-> 1. every basic prototype: `P ⊆ T`
+> 1. every basic value: `P ⊆ T`
 > 1. every constraint in `𝒞`<sub>`Label`</sub> is a term: `𝒞`<sub>`Label`</sub>` ⊆ T`
 >    a _reference_ may refer to any substructure of `C`.
-> 1. for every `n` prototypes `t₁, ..., tₙ`, and every `n`-ary function symbol
->    `f ∈ F_n`, the prototype `f(t₁,...,tₙ) ∈ T`.
+> 1. for every `n` values `t₁, ..., tₙ`, and every `n`-ary function symbol
+>    `f ∈ F_n`, the value `f(t₁,...,tₙ) ∈ T`.
 >
 
 
@@ -2202,19 +2173,19 @@
 Multiple labels may be recursively combined in any order.
 
 <!-- unnecessary, probably.
-#### Definition of evaluated prototype
+#### Definition of evaluated value
 
-> A fully evaluated prototype, `T_evaluated ⊆ T` is a subset of `T` consisting
+> A fully evaluated value, `T_evaluated ⊆ T` is a subset of `T` consisting
 > only of atoms, typed attribute structures and constraint functions.
 >
-> A prototype is called _ground_ if it is an atom or typed attribute structure.
+> A value is called _ground_ if it is an atom or typed attribute structure.
 
-#### Unification of evaluated prototypes
+#### Unification of evaluated values
 
-> A fully evaluated prototype, `T_evaluated ⊆ T` is a subset of `T` consisting
+> A fully evaluated value, `T_evaluated ⊆ T` is a subset of `T` consisting
 > only of atoms, typed attribute structures and constraint functions.
 >
-> A prototype is called _ground_ if it is an atom or typed attribute structure.
+> A value is called _ground_ if it is an atom or typed attribute structure.
 -->
 
 #### Definition of subsumption and unification on typed attribute structure
@@ -2241,7 +2212,7 @@
 sufficiently precise. Although I admit that references and cycles
 are still unclear to me. -->
 
-Like with the subsumption relation for basic prototypes,
+Like with the subsumption relation for basic values,
 the subsumption relation for constraints determines the mutual placement
 of constraints within the partial order of all values.