diff --git a/content/blog/05_spa_agda_semantics/index.md b/content/blog/05_spa_agda_semantics/index.md
index 944fa17..f58d0a5 100644
--- a/content/blog/05_spa_agda_semantics/index.md
+++ b/content/blog/05_spa_agda_semantics/index.md
@@ -418,13 +418,52 @@ to evaluate the _expression_ that serves as the condition. We then had an
 additional premise that requires the truthiness of the resulting value \(v\).
 The rule for evaluating a conditional with a "false" branch is very similar.
 
-
 {{< latex >}}
 \frac
     { \rho_1 , e \Downarrow v \quad v = 0 \quad \rho_1, s_2 \Rightarrow \rho_2}
     { \rho_1, \textbf{if}\ e\ \{ s_1 \}\ \textbf{else}\ \{ s_2 \}\ \Rightarrow \rho_2 }
 {{< /latex >}}
 
+Now that we have rules for conditional statements, it will be surprisingly easy
+to define the rules for `while` loops. A `while` loop will also have two rules,
+one for when its condition is truthy and one for when it's falsey. However,
+unlike the "false" case, a while loop will do nothing, leaving the environment
+unchanged:
+
+{{< latex >}}
+\frac
+    { \rho_1 , e \Downarrow v \quad v = 0 }
+    { \rho_1 , \textbf{while}\ e\ \{ s \}\ \Rightarrow \rho_1 }
+{{< /latex >}}
+
+The trickiest rule is for when the condition of a `while` loop is true.
+We evaluate the body once, starting in environment \(\rho_1\) and finishing
+in \(\rho_2\), but then we're not done. In fact, we have to go back to the top,
+and check the condition again, starting over. As a result, we include another
+premise, that tells us that evaluating the loop starting at \(\rho_2\), we
+eventually end in state \(\rho_3\). This encodes the "rest of the iterations"
+in addition to the one we just performed. The environment \(\rho_3\) is our
+final state, so that's what we use in the rule's conclusion.
+
+{{< latex >}}
+\frac
+    { \rho_1 , e \Downarrow v \quad v \neq 0 \quad \rho_1 , s \Rightarrow \rho_2 \quad \rho_2 , \textbf{while}\ e\ \{ s \}\ \Rightarrow \rho_3 }
+    { \rho_1 , \textbf{while}\ e\ \{ s \}\ \Rightarrow \rho_3 }
+{{< /latex >}}
+
+And that's it! We have now seen every rule that defines the little object language
+I've been using for my Agda work. As with all the other rules we've seen, the
+mathematical notation above can be directly translated into Agda:
+
+{{< codelines "Agda" "agda-spa/Language/Semantics.agda" 47 64 >}}
+
+Below is a Bergamot widget that implements these rules. Try the following program,
+which computes the `x`th power of two, and stores it in `y`:
+
+```
+x = 5; y = 1; while (x) { y = y + y; x = x - 1 }
+```
+
 {{< bergamot_widget id="stmt-widget" query="" prompt="step(extend(extend(extend(empty, x, 17), y, 42), z, 0), TERM, ?env)" modes="Statement:Statement" >}}
 hidden section "" {
   Eq @ eq(?x, ?x) <-;
@@ -460,3 +499,31 @@ hidden section "" {
   EnvSkip @ inenv(?x, ?v_1, extend(?rho, ?y, ?v_2)) <- inenv(?x, ?v_1, ?rho), not(eq(?x, ?y));
 }
 {{< /bergamot_widget >}}
+
+### Semantics as Ground Truth
+
+Prior to this post, we had been talking about using lattices and monotone
+functions for program analysis. The key problem with using this framework to
+define analyses is that there are many monotone functions that produce complete
+nonsese; their output is, at best, unrelated to the program they're supposed
+to analyze. We don't want to write such functions, since having incorrect
+information about the programs in question is unhelpful.
+
+What does it mean for a function to produce correct information, though?
+In the context of sign analysis, it would mean that if we say a variable `x` is `+`,
+then evaluating the program will leave us in a state in which `x` is posive.
+The semantics we defined in this post give us the "evaluating the program piece".
+They establish what the programs _actually_ do, and we can use this ground
+truth when checking that our analyses are correct. In subsequent posts, I will
+prove the exact property I informally stated above: __for the program analyses
+we define, things they "claim" about our program will match what actually happens
+when executing the program using our semantics__.
+
+A piece of the puzzle still remains: how are we going to use the monotone
+functions we've been talking so much about? We need to figure out what to feed
+to our analyses before we can prove their correctness.
+
+I have an answer to that question: we will be using _control flow graphs_ (CFGs).
+These are another program representation, one that's more commonly found in
+compilers. I will show what they look like in the next post. I hope to see you
+there!