sarvex
diff --git a/‎specification/terms.md
Lines changed: 39 additions & 34 deletions b/‎specification/terms.md
Lines changed: 39 additions & 34 deletions
@@ -77,22 +77,25 @@ If a vexpr is used where an lexpr is expected (other than the LHS of an assignme
 A typed expression that evaluates to an value, as opposed to an object. The RHS of an assignment and the arguments of a function are examples of vexprs.
 
 NOTE: Because of evaluation order concerns, after being potentially wrapped to a
-vexpr, subexpressions are often wrapped in a `VExpr::Use(LExpr::Temp(vexpr))`. The
+vexpr, subexpressions are often wrapped in a `Use(Temp(vexpr))`. The
 exact rules here should be documented.
 
 If a lexpr is used where an vexpr is expected, it is wrapped in an implicit use
 vexpr, the rules of which are given in §2.3.
 
 ### §2.3 Temporary lexpr
 
-```Rust
-    LExpr::Temp(VExpr)
+```
+Temp:
+    Γ ⊢ vexp VExpr
+    --------------
+    Γ ⊢ Temp(vexp) LExpr
 ```
 
 An implicit lexpr that wraps a vexpr when an lexpr is expected.
  When evaluated, it:
 
- * creates a temporary object, scheduled for destruction at the end of the current temporary scope.
+ * creates a temporary object within the arena selected by the arena specification.
  * evaluates the vexpr and stores it within the object.
  * evaluates to the temporary object.
 
@@ -111,8 +114,11 @@ fn main() {
 
 ### §2.4 Use vexpr
 
-```Rust
-    VExpr::Use(LExpr)
+```
+Use:
+    Γ ⊢ vexp VExpr
+    --------------
+    Γ ⊢ Use(vexp) LExpr
 ```
 
 An implicit vexpr that wraps a lexpr when a vexpr is expected.
@@ -126,31 +132,12 @@ If the value read is an `undef`, behavior is undefined unless the expression's
 type is an integer, in which case behavior is unspecified (FIXME: this is intended
 to allow reads from padding - what can we say here?).
 
-The read-from object must be aligned to `align_of::<T>()` or behavior is undefined.
+The read-from object must be aligned to `AlignOf(T)` or behavior is undefined.
 
 If the expression's type does not implement `Copy`, the value is moved out of the
 object, preventing further accesses.
 
-### §2.5 Destruction scopes
-
-A Rust function always keeps a chain of destruction scopes. Each destruction scope contains a list of objects - temporaries and variables - that are to be destroyed when that scope is exited.
-
-The objects in a scope are dropped in the reverse order of their insertion. If such an object is in an uninitialized state (either because it was never initialized or because it was moved out of), it is not destroyed again.
-
-If one of the destructors panics, the current scope as well as the remaining scopes
-are exited and the panic continues to unwind.
-
-### §2.5.1 Temporary scopes
-
-A set of baroque rules assigns a destruction scope, called the *temporary scope*,
-to each expression.
-
-FIXME: explain these rules.
-
-The temporary created by `LExpr::Temp` is added to that expression's temporary
-scope's destruction list.
-
-### §2.6 Note on the terms lvalue and rvalue
+### §2.5 Note on the terms lvalue and rvalue
 
 These terms aren't used in this document, because they are used in conflicting ways in various places. However, lvalue is equivalent to lexpr, while rvalue is equivalent to vexpr.
 
@@ -162,37 +149,55 @@ An object is an untyped, contiguous block of memory with a certain size and a ce
 
 All objects are able to be read, but you may not write to all objects.
 
-A lexpr associated with an object, as a vexpr, will evaluate to a value (see §4) that is equivalent to the memory of the object, interpreted as the type of the lexpr.
+A `Use` vexpr, applied to a lexpr that evaluates to an object, will evaluate to a value (see §4) that is equivalent to the memory of the object, interpreted as the type of the vexpr.
 
-A write to an object will set the memory of that object equivalent to the value of the write, without the interpretation of typing.
+A write to an object will set the memory of that object equivalent to the value of the write, without the interpretation of typing. (XXX: padding on assignment).
 
 ### §3.2 Allocation.
 
-An object may be allocated in one of three ways:
+Objects may be created in the following ways, which create objects that do not overlap as long as they are valid.
+
+There may be other (implementation-defined and/or unspecified) ways to create objects.
+
+### §3.2.1 Statics
 
-In static memory:
+Statics are valid until the end of the program. For example,
 
 ```rust
 static x: i32 = 0i32; // a static, read-only object of size >= 4, alignment >= 4
 static mut x: i32 = 0i32; // a static, read-write object of size >= 4, alignment >= 4
 static x: AtomicI32 = 0i32; // a static, read-write object of size >= 4, alignment >= 4
 ```
 
-on the stack:
+### §3.2.2 Locals
+
+Locals include argument buffers, temporaries, and named bindings. They are always allocated into an arena (§3.3) and are valid until destroyed by it.
+
+For example:
 
 ```rust
 let x: i32 = 0i32; // a stack, read-only object of size >= 4, alignment >= 4
 // you get the point
 ```
 
-or on the heap:
+### §3.2.3 Heap Allocations
+
+Each call to `Box::new` creates a heap allocation, which is valid until it is destroyed when the box is dropped.
+
+For example:
 
 ```rust
 let x: Box<i32> = Box::new(0i32); // a stack, read-only object pointing to a heap,
                                   // read-write object of size >= 4, alignment >= 4
 ```
 
-### §3.3 Note on types:
+### §3.3 Arenas
+
+A function's stack of arenas is used to manage the orderly destruction of the locals within that function.
+
+See [the arena specification](https://github.com/nikomatsakis/rust-memory-model/issues/17) for more details (XXX: write it somewhere more permanent).
+
+### §3.4 Note on types:
 
 Objects *are not* typed. No, not even effective types ^-^