diff --git a/lang/spec.html b/lang/spec.html
index db759327..d421057d 100644
--- a/lang/spec.html
+++ b/lang/spec.html
@@ -8221,7 +8221,7 @@ <h3>Worker message passing</h3>
 could be executed more than once.
 </p>
 <p>
-There are three types determined at compile-time for each slot:
+There are four types determined at compile-time for each slot:
 </p>
 <ul>
 <li>a message type: if a message v is written to the slot, then v belongs to the
@@ -8233,7 +8233,7 @@ <h3>Worker message passing</h3>
 <li>a send failure type: this is the type of termination failure in the sending
 worker that caused the corresponding message not to be sent; more precisely, for
 any slot index <var>i</var>, if it is possible for <var>i</var> to be &#x2265;
-the value of index <var>w</var> of the queue at the time when the sending worker
+the index <var>w</var> of the queue at the time when the sending worker
 completes normally with termination value <var>e</var>, then <var>e</var>
 belongs to the send failure type of the slot with index <var>i</var>; it is a
 compile-time error if the send failure type is not a (possibly empty) subtype of
@@ -8241,7 +8241,7 @@ <h3>Worker message passing</h3>
 <li>a receive failure type: this is the type of termination failure in the
 receiving worker that caused the corresponding message not to be received; more
 precisely, for any slot index <var>i</var>, if it is possible for <var>i</var>
-to be &#x2265; the value of index <var>r</var> of the queue at the time when the
+to be &#x2265; the index <var>r</var> of the queue at the time when the
 receiving worker completes normally with termination value <var>e</var>, then
 <var>e</var> belongs to the receive failure type of the slot with index
 <var>i</var>; it is a compile-time error if the receive failure type is not a
@@ -8349,8 +8349,8 @@ <h5>Flush action</h5>
 A flush-action with peer-worker R occurring within worker W is associated with the
 queue with sending worker W and receiving worker R. Evaluating
 the flush-action flushes the queue up to index
-<var>i</var> where <var>k</var> is the number of send-actions in W that syntactically
-precede the flush-action. More precisely, the evaluation of a flush-action waits until
+<var>i</var> where <var>i</var> is the number of send-actions in W that syntactically
+precede the flush-action. More precisely, the evaluation of a flush-action waits
 until either the index <var>r</var> of the queue is &#x2265;
 <var>i</var> or the receiving worker has terminated. It then completes as
 follows: