Edit the Dawn post a bit

content/blog/coq_dawn.md

@@ -14,7 +14,7 @@ and that's what I reached for when making this attempt.
 
 ### Defining the Syntax
 #### Expressions and Intrinsics
-For the most part, this is the easy part. A Dawn expression is one of three things:
+This is mostly the easy part. A Dawn expression is one of three things:
 
 * An "intrinsic", written \\(i\\), which is akin to a built-in function or command.
 * A "quote", written \\([e]\\), which takes a Dawn expression \\(e\\) and moves it onto the stack (Dawn is stack-based).
@@ -45,7 +45,7 @@ Why do we need `e_int`? We do because a token like \\(\\text{swap}\\) can be vie
 as belonging to the set of intrinsics \\(i\\), or the set of expressions, \\(e\\). While writing
 down the rules in mathematical notation, what exactly the token means is inferred from context - clearly
 \\(\\text{swap}\\ \\text{drop}\\) is an expression built from two other expressions. In statically-typed
-functional languages (like Coq or Haskell), however, the same expression can't belong to two different,
+functional languages like Coq or Haskell, however, the same expression can't belong to two different,
 arbitrary types. Thus, to turn an intrinsic into an expression, we need to wrap it up in a constructor,
 which we called `e_int` here. Other than that, `e_quote` accepts as argument another expression, `e` (the
 thing being quoted), and `e_comp` accepts two expressions, `e1` and `e2` (the two sub-expressions being composed).
@@ -59,7 +59,7 @@ names are reserved in Coq, we can just call our constructors exactly the same as
 in the written formalization.
 
 #### Values and Value Stacks
-Values are up next. My initial temptation was to define a value much like
+Values are up next. My initial thought was to define a value much like
 I defined an intrinsic expression: by wrapping an expression in a constructor for a new data
 type. Something like:
 
@@ -245,7 +245,7 @@ I invite you to take a look at the "shape" of the proof:
     `Sem_e_int`, which handles the intrinsic case. This, in turn, requires that we show
     the effect of the intrinsic itself; the `apply` intrinsic evaluates the quoted expression
     on the stack.
-    The quoted expression is contains the body of false, or \\(\\text{drop}\\). This is
+    The quoted expression contains the body of false, or \\(\\text{drop}\\). This is
     once again an intrinsic, so we use `Sem_e_int`; the intrinsic in question is \\(\\text{drop}\\),
     so the `Sem_drop` rule takes care of that.
 
@@ -277,7 +277,7 @@ Similarly, we prove that \\(\\text{or}\\) applied to \\(\\text{true}\\) always r
 
 {{< codelines "Coq" "dawn/Dawn.v" 75 83 >}}
 
-Finally, the specific facts (like \\(\\text{false}\\ \\text{or} \\text{false}\\) evaluating to \\(\\text{false}\\))
+Finally, the specific facts (like \\(\\text{false}\\ \\text{or}\\ \\text{false}\\) evaluating to \\(\\text{false}\\))
 can be expressed using our two new proofs, `or_false_v` and `or_true`.
 
 {{< codelines "Coq" "dawn/Dawn.v" 85 88 >}}
@@ -292,7 +292,7 @@ on the stack. This is defined in terms of other Dawn expressions as follows:
 \text{quote}_n = \text{quote}_{n-1}\ \text{swap}\ \text{quote}\ \text{swap}\ \text{compose}
 {{< /latex >}}
 
-We can define this in Coq as follows:
+We can write this in Coq as follows:
 
 {{< codelines "Coq" "dawn/Dawn.v" 90 94 >}}
 
@@ -330,7 +330,7 @@ Thus, it will try `Sem_swap` if the expression is \\(\\text{swap}\\),
 {{< codelines "Coq" "dawn/Dawn.v" 138 144 >}}
 
 #### Rotations
-There's a little trick to formalizing rotations. There's an important property of values:
+There's a little trick to formalizing rotations. Values have an important property:
 when a value is run against a stack, all it does is place itself on a stack. We can state
 this as follows:
 
@@ -353,21 +353,22 @@ placed back on the stack.
 {{< codelines "Coq" "dawn/Dawn.v" 156 168 >}}
 
 ### `e_comp` is Associative
-When composing three expressions, which way of pressing parentheses is correct?
+When composing three expressions, which way of inserting parentheses is correct?
-Is it \\((e_1\\ e_2)\\ e_3\\)? Or is it \\(e_1\\ (e_2\\ e_3)\\)? Well, neither!
+Is it \\((e_1\\ e_2)\\ e_3\\)? Or is it \\(e_1\\ (e_2\\ e_3)\\)? Well, both!
 Expression composition is associative, which means that the order of the parentheses
 doesn't matter. We state this in the following theorem, which says that the two
 ways of writing the composition, if they evaluate to anything, evaluate to the same thing.
 
 {{< codelines "Coq" "dawn/Dawn.v" 170 171 >}}
 
+### Conclusion
 That's all I've got in me for today. However, we got pretty far! The Dawn specification
 says:
 
 > One of my long term goals for Dawn is to democratize formal software verification in order to make it much more feasible and realistic to write perfect software.
 
 I think that Dawn is definitely getting there: formally defining the semantics outlined
-on the page was quite straightforward! We can now have complete confidence in the behavior
+on the page was quite straightforward. We can now have complete confidence in the behavior
 of \\(\\text{true}\\), \\(\\text{false}\\), \\(\\text{or}\\), \\(\\text{quote}_n\\) and
 \\(\\text{rotate}_n\\). The proof of associativity is also enough to possibly argue for simplifying
 the core calculus' syntax even more. All of this we got from an official source, with only