diff --git a/content/blog/coq_dawn_eval/index.md b/content/blog/coq_dawn_eval/index.md
index 8286bb6..5e7a32e 100644
--- a/content/blog/coq_dawn_eval/index.md
+++ b/content/blog/coq_dawn_eval/index.md
@@ -1,13 +1,12 @@
 ---
 title: "A Verified Evaluator for the Untyped Concatenative Calculus"
 date: 2021-11-27T20:24:57-08:00
-draft: true
 tags: ["Dawn", "Coq", "Programming Languages"]
 ---
 
 Earlier, I wrote [an article]({{< relref "./coq_dawn" >}}) in which I used Coq to
 encode the formal semantics of [Dawn's Untyped Concatenative Calculus](https://www.dawn-lang.org/posts/foundations-ucc/),
-and to prove a few thing about the mini-language. Though I'm quite happy with how that turned out,
+and to prove a few things about the mini-language. Though I'm quite happy with how that turned out,
 my article was missing something that's present on the original Dawn page -- an evaluator. In this article, I'll define
 an evaluator function in Coq, prove that it's equivalent to Dawn's formal semantics,
 and extract all of this into usable Haskell code.
@@ -150,7 +149,7 @@ data Value =
 ```
 
 All that's left is to make a new file, `Ucc.hs`. I use a different file so that
-changes I make aren't overridden by Coq each time I run extraction. In this
+Coq doesn't overwrite my changes every time I re-run extraction. In this
 file, we place the "glue code" that tries running one step after another:
 
 {{< codelines "Coq" "dawn/Ucc.hs" 46 51 >}}
@@ -196,7 +195,7 @@ Thus, we have two possibilities:
 
   {{< codelines "Coq" "dawn/DawnEval.v" 31 33 >}}
 
-The whole theorem claim is as follows:
+The whole theorem statement is as follows:
 
 {{< codelines "Coq" "dawn/DawnEval.v" 29 33 >}}
 
@@ -247,7 +246,7 @@ exists ei1 ei2 vsi1 vsi2,
 I can imagine that you're getting the idea, but here's one last picture:
 {{< figure src="coq_eval_two.png" caption="Visual representation of a three-step evaluation." class="small" alt="Four dots connected by lines. The first dot is labeled \"vs\", the next \"vsi1\", the one after \"vsi2\", and the last \"vs1\". The second and third dots are highlighted." >}}
 
-This is awful! Not only is this a lot of writing, but it also makes various
+The Coq code for this is awful! Not only is this a lot of writing, but it also makes various
 sequences of steps have a different "shape". This way, we can't make
 proofs about evaluations of an _arbitrary_ number of steps. Not all is lost, though: if we squint
 a little at the last example (three steps), a pattern starts to emerge.
@@ -598,7 +597,7 @@ $ ./Ucc
 ```
 
 ### Potential Future Work
-We now have a verified UCC evaluator in Haskell. What now?
+We now have a verified UCC evaluator in Haskell. What next?
 
 1. We only verified the evaluation component of our REPL. In fact,
    the whole thing is technically a bit buggy due to the parser: