Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Edit and publish second Coq Dawn article

Browse Source
This commit is contained in:
Danila Fedorin 2021-12-02 18:29:47 -08:00
parent b8f9f93537
commit 13aef5b3c0
1 changed files with 5 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
content/blog/coq_dawn_eval/index.md
View File

@ -1,13 +1,12 @@
--- ---
title: "A Verified Evaluator for the Untyped Concatenative Calculus" title: "A Verified Evaluator for the Untyped Concatenative Calculus"
date: 2021-11-27T20:24:57-08:00 date: 2021-11-27T20:24:57-08:00
draft: true
tags: ["Dawn", "Coq", "Programming Languages"] tags: ["Dawn", "Coq", "Programming Languages"]
--- ---
Earlier, I wrote [an article]({{< relref "./coq_dawn" >}}) in which I used Coq to 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/), 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 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, an evaluator function in Coq, prove that it's equivalent to Dawn's formal semantics,
and extract all of this into usable Haskell code. 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 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: file, we place the "glue code" that tries running one step after another:
{{< codelines "Coq" "dawn/Ucc.hs" 46 51 >}} {{< codelines "Coq" "dawn/Ucc.hs" 46 51 >}}
@ -196,7 +195,7 @@ Thus, we have two possibilities:
{{< codelines "Coq" "dawn/DawnEval.v" 31 33 >}} {{< 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 >}} {{< 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: 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." >}} {{< 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 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 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. a little at the last example (three steps), a pattern starts to emerge.
@ -598,7 +597,7 @@ $ ./Ucc
``` ```
### Potential Future Work ### 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, 1. We only verified the evaluation component of our REPL. In fact,
the whole thing is technically a bit buggy due to the parser: the whole thing is technically a bit buggy due to the parser: