From 13aef5b3c03691c0d4b578e89a0ab023c3c38fc2 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 2 Dec 2021 18:29:47 -0800 Subject: [PATCH] Edit and publish second Coq Dawn article --- content/blog/coq_dawn_eval/index.md | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) 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: