Note about reversing order

_site/essays/2018-01-16-how-to-prove-a-compiler-correct.html

@@ -64,7 +64,7 @@ <h3 id="dsl-compiler">DSL &amp; Compiler</h3>
 compile (<span class="dt">Plus</span> a1 a2)  <span class="fu">=</span> compile a2 <span class="fu">++</span> compile a1 <span class="fu">++</span> [<span class="dt">SPlus</span>]
 compile (<span class="dt">Minus</span> a1 a2) <span class="fu">=</span> compile a2 <span class="fu">++</span> compile a1 <span class="fu">++</span> [<span class="dt">SMinus</span>]
 compile (<span class="dt">Times</span> a1 a2) <span class="fu">=</span> compile a2 <span class="fu">++</span> compile a1 <span class="fu">++</span> [<span class="dt">STimes</span>]</code></pre></div>
-<p>The cases for plus/minus/times are the cases that are slightly non-obvious, because they can contain further recursive expressions, but if you think about what the <code>eval</code> function is doing, once the stack machine <em>finishes</em> evaluating everything that <code>a1</code> compiled to, the number that the left branch evaluated to should be on the top of the stack. Then once it finishes evaluating what <code>a2</code> compiles to the number that the right branch evaluated to should be on the top of the stack. This means that evaluating e.g. <code>SPlus</code> will put the sum on the top of the stack, as expected. That’s a pretty informal argument about correctness, but we’ll have a chance to get more formal later.</p>
+<p>The cases for plus/minus/times are the cases that are slightly non-obvious, because they can contain further recursive expressions, but if you think about what the <code>eval</code> function is doing, once the stack machine <em>finishes</em> evaluating everything that <code>a2</code> compiled to, the number that the left branch evaluated to should be on the top of the stack. Then once it finishes evaluating what <code>a1</code> compiles to the number that the right branch evaluated to should be on the top of the stack (the reversal is so that they are in the right order when popped off). This means that evaluating e.g. <code>SPlus</code> will put the sum on the top of the stack, as expected. That’s a pretty informal argument about correctness, but we’ll have a chance to get more formal later.</p>
 <h2 id="formalizing">Formalizing</h2>
 <p>Now that we have a Haskell compiler, we want to prove it correct! So what do we do? First, we want to convert this to Coq using the <a href="https://github.com/antalsz/hs-to-coq">hs-to-coq</a> tool. There are full instructions at <a href="https://github.com/dbp/howtoproveacompiler" class="uri">https://github.com/dbp/howtoproveacompiler</a>, but the main command that will convert <code>src/Compiler.hs</code> to <code>src/Compiler.v</code>:</p>
 <pre><code>STACK_YAML=hs-to-coq/stack.yaml stack exec hs-to-coq -- -o src/ src/Compiler.hs -e hs-to-coq/base/edits</code></pre>

_site/rss.xml

@@ -51,7 +51,7 @@ compile (<span class="dt">Num</span> n)       <span class="fu">=</span> [<span c
 compile (<span class="dt">Plus</span> a1 a2)  <span class="fu">=</span> compile a2 <span class="fu">++</span> compile a1 <span class="fu">++</span> [<span class="dt">SPlus</span>]
 compile (<span class="dt">Minus</span> a1 a2) <span class="fu">=</span> compile a2 <span class="fu">++</span> compile a1 <span class="fu">++</span> [<span class="dt">SMinus</span>]
 compile (<span class="dt">Times</span> a1 a2) <span class="fu">=</span> compile a2 <span class="fu">++</span> compile a1 <span class="fu">++</span> [<span class="dt">STimes</span>]</code></pre></div>
-<p>The cases for plus/minus/times are the cases that are slightly non-obvious, because they can contain further recursive expressions, but if you think about what the <code>eval</code> function is doing, once the stack machine <em>finishes</em> evaluating everything that <code>a1</code> compiled to, the number that the left branch evaluated to should be on the top of the stack. Then once it finishes evaluating what <code>a2</code> compiles to the number that the right branch evaluated to should be on the top of the stack. This means that evaluating e.g. <code>SPlus</code> will put the sum on the top of the stack, as expected. That’s a pretty informal argument about correctness, but we’ll have a chance to get more formal later.</p>
+<p>The cases for plus/minus/times are the cases that are slightly non-obvious, because they can contain further recursive expressions, but if you think about what the <code>eval</code> function is doing, once the stack machine <em>finishes</em> evaluating everything that <code>a2</code> compiled to, the number that the left branch evaluated to should be on the top of the stack. Then once it finishes evaluating what <code>a1</code> compiles to the number that the right branch evaluated to should be on the top of the stack (the reversal is so that they are in the right order when popped off). This means that evaluating e.g. <code>SPlus</code> will put the sum on the top of the stack, as expected. That’s a pretty informal argument about correctness, but we’ll have a chance to get more formal later.</p>
 <h2 id="formalizing">Formalizing</h2>
 <p>Now that we have a Haskell compiler, we want to prove it correct! So what do we do? First, we want to convert this to Coq using the <a href="https://github.com/antalsz/hs-to-coq">hs-to-coq</a> tool. There are full instructions at <a href="https://github.com/dbp/howtoproveacompiler" class="uri">https://github.com/dbp/howtoproveacompiler</a>, but the main command that will convert <code>src/Compiler.hs</code> to <code>src/Compiler.v</code>:</p>
 <pre><code>STACK_YAML=hs-to-coq/stack.yaml stack exec hs-to-coq -- -o src/ src/Compiler.hs -e hs-to-coq/base/edits</code></pre>

essays/2018-01-16-how-to-prove-a-compiler-correct.markdown

@@ -112,13 +112,13 @@ compile (Times a1 a2) = compile a2 ++ compile a1 ++ [STimes]
 The cases for plus/minus/times are the cases that are slightly non-obvious,
 because they can contain further recursive expressions, but if you think about
 what the `eval` function is doing, once the stack machine _finishes_ evaluating
-everything that `a1` compiled to, the number that the left branch evaluated to
-should be on the top of the stack. Then once it finishes evaluating what `a2`
+everything that `a2` compiled to, the number that the left branch evaluated to
+should be on the top of the stack. Then once it finishes evaluating what `a1`
 compiles to the number that the right branch evaluated to should be on the top
-of the stack. This means that evaluating e.g. `SPlus` will put the
-sum on the top of the stack, as expected. That's a pretty informal
-argument about correctness, but we'll have a chance to get more formal
-later.
+of the stack (the reversal is so that they are in the right order when popped
+off). This means that evaluating e.g. `SPlus` will put the sum on the top of the
+stack, as expected. That's a pretty informal argument about correctness, but
+we'll have a chance to get more formal later.
 
 ## Formalizing