Tweaks

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

@@ -28,12 +28,13 @@ <h2>How to prove a compiler correct</h2>
 
 <p>by <em>Daniel Patterson</em> on <strong>January 16, 2018</strong></p>
 
-<p>At POPL’18 (Principles of Programming Languages) last week, I ended up talking to <a href="https://anniecherkaev.com">Annie Cherkaev</a> about her really cool DSL (domain specific language) <a href="https://github.com/anniecherk/sweetpea">SweetPea</a>, which is a “SAT-Sampler aided language for experimental design, targeted for Psychology &amp; Neuroscience”. In particular, we were talking about software engineering, and the work that Annie was doing to test SweetPea and increase her confidence that the implementation is correct! The topic of how exactly one goes about proving a compiler correct came up, and I realized that I couldn’t think of a high-level (but <em>concrete</em>) overview of what that might look like. Also, like many compilers, hers is implemented in Haskell, so it seemed like a good opportunity to try out the really cool work presented at the colocated conference CPP’18 (Certified Programs and Proofs) titled <a href="https://arxiv.org/abs/1711.09286">“Total Haskell is Reasonable Coq” by Spector-Zabusky, Breitner, Rizkallah, and Weirich</a>. They have a tool (<code>hs-to-coq</code>) that extracts Coq definitions from (certain) terminating Haskell programs (of which at least small compilers hopefully qualify).</p>
+<p>At POPL’18 (Principles of Programming Languages) last week, I ended up talking to <a href="https://anniecherkaev.com">Annie Cherkaev</a> about her really cool DSL (domain specific language) <a href="https://github.com/anniecherk/sweetpea">SweetPea</a>, which is a “SAT-Sampler aided language for experimental design, targeted for Psychology &amp; Neuroscience”. In particular, we were talking about software engineering, and the work that Annie was doing to test SweetPea and increase her confidence that the implementation is correct! The topic of how exactly one goes about proving a compiler correct came up, and I realized that I couldn’t think of a high-level (but <em>concrete</em>) overview of what that might look like. Also, like many compilers, hers is implemented in Haskell, so it seemed like a good opportunity to try out the really cool work presented at the colocated conference CPP’18 (Certified Programs and Proofs) titled <a href="https://arxiv.org/abs/1711.09286">“Total Haskell is Reasonable Coq” by Spector-Zabusky, Breitner, Rizkallah, and Weirich</a>. They have a tool (<code>hs-to-coq</code>) that extracts Coq definitions from (certain) terminating Haskell programs (of which at least small compilers hopefully qualify). There are certainly limitations to this approach (see Addendum at the bottom of the page for some discussion), but it seems very promising from an engineering perspective.</p>
 <p>The intention of this post is twofold:</p>
 <ol style="list-style-type: decimal">
 <li>Show how to take a compiler (albeit a tiny one) that was built with no intention of verifying it and after the fact prove it correct. Part of the ability to do this in such a seamless way is the wonderful <code>hs-to-coq</code> tool mentioned above, though there is no reason in principle you couldn’t carry out this translation manually (in practice maintenance becomes an issue, hence realistic verified compilers relying on writing their implementations within theorem provers like Coq and then <em>extracting</em> executable versions automatically, at least in the past – possibly <code>hs-to-coq</code> could change this workflow).</li>
 <li>Give a concrete example of proving compiler correctness. By necessity, this is a very simplified scenario without a lot of the subtleties that appear in real verification efforts (e.g., undefined behavior, multiple compiler passes, linking with code after compilation, etc). On the other hand, even this simplified scenario could cover many cases of DSLs, and understanding the subtleties that come up should be much easier once you understand the basic case!</li>
 </ol>
+<p><strong>The intended audience is: people who know what compilers are (and may have implemented them!) but aren’t sure what it means to prove one correct!</strong></p>
 <blockquote>
 <p>All the code for this post, along with instructions to get it running, is in the repository <a href="https://github.com/dbp/howtoproveacompiler" class="uri">https://github.com/dbp/howtoproveacompiler</a>. If you have any trouble getting it going, open an issue on that repository.</p>
 </blockquote>

_site/rss.xml

@@ -15,12 +15,13 @@
 
 <p>by <em>Daniel Patterson</em> on <strong>January 16, 2018</strong></p>
 
-<p>At POPL’18 (Principles of Programming Languages) last week, I ended up talking to <a href="https://anniecherkaev.com">Annie Cherkaev</a> about her really cool DSL (domain specific language) <a href="https://github.com/anniecherk/sweetpea">SweetPea</a>, which is a “SAT-Sampler aided language for experimental design, targeted for Psychology &amp; Neuroscience”. In particular, we were talking about software engineering, and the work that Annie was doing to test SweetPea and increase her confidence that the implementation is correct! The topic of how exactly one goes about proving a compiler correct came up, and I realized that I couldn’t think of a high-level (but <em>concrete</em>) overview of what that might look like. Also, like many compilers, hers is implemented in Haskell, so it seemed like a good opportunity to try out the really cool work presented at the colocated conference CPP’18 (Certified Programs and Proofs) titled <a href="https://arxiv.org/abs/1711.09286">“Total Haskell is Reasonable Coq” by Spector-Zabusky, Breitner, Rizkallah, and Weirich</a>. They have a tool (<code>hs-to-coq</code>) that extracts Coq definitions from (certain) terminating Haskell programs (of which at least small compilers hopefully qualify).</p>
+<p>At POPL’18 (Principles of Programming Languages) last week, I ended up talking to <a href="https://anniecherkaev.com">Annie Cherkaev</a> about her really cool DSL (domain specific language) <a href="https://github.com/anniecherk/sweetpea">SweetPea</a>, which is a “SAT-Sampler aided language for experimental design, targeted for Psychology &amp; Neuroscience”. In particular, we were talking about software engineering, and the work that Annie was doing to test SweetPea and increase her confidence that the implementation is correct! The topic of how exactly one goes about proving a compiler correct came up, and I realized that I couldn’t think of a high-level (but <em>concrete</em>) overview of what that might look like. Also, like many compilers, hers is implemented in Haskell, so it seemed like a good opportunity to try out the really cool work presented at the colocated conference CPP’18 (Certified Programs and Proofs) titled <a href="https://arxiv.org/abs/1711.09286">“Total Haskell is Reasonable Coq” by Spector-Zabusky, Breitner, Rizkallah, and Weirich</a>. They have a tool (<code>hs-to-coq</code>) that extracts Coq definitions from (certain) terminating Haskell programs (of which at least small compilers hopefully qualify). There are certainly limitations to this approach (see Addendum at the bottom of the page for some discussion), but it seems very promising from an engineering perspective.</p>
 <p>The intention of this post is twofold:</p>
 <ol style="list-style-type: decimal">
 <li>Show how to take a compiler (albeit a tiny one) that was built with no intention of verifying it and after the fact prove it correct. Part of the ability to do this in such a seamless way is the wonderful <code>hs-to-coq</code> tool mentioned above, though there is no reason in principle you couldn’t carry out this translation manually (in practice maintenance becomes an issue, hence realistic verified compilers relying on writing their implementations within theorem provers like Coq and then <em>extracting</em> executable versions automatically, at least in the past – possibly <code>hs-to-coq</code> could change this workflow).</li>
 <li>Give a concrete example of proving compiler correctness. By necessity, this is a very simplified scenario without a lot of the subtleties that appear in real verification efforts (e.g., undefined behavior, multiple compiler passes, linking with code after compilation, etc). On the other hand, even this simplified scenario could cover many cases of DSLs, and understanding the subtleties that come up should be much easier once you understand the basic case!</li>
 </ol>
+<p><strong>The intended audience is: people who know what compilers are (and may have implemented them!) but aren’t sure what it means to prove one correct!</strong></p>
 <blockquote>
 <p>All the code for this post, along with instructions to get it running, is in the repository <a href="https://github.com/dbp/howtoproveacompiler" class="uri">https://github.com/dbp/howtoproveacompiler</a>. If you have any trouble getting it going, open an issue on that repository.</p>
 </blockquote>

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

@@ -6,18 +6,21 @@ author: Daniel Patterson
 At POPL'18 (Principles of Programming Languages) last week, I ended up talking
 to [Annie Cherkaev](https://anniecherkaev.com) about her really cool DSL (domain
 specific language) [SweetPea](https://github.com/anniecherk/sweetpea), which is
-a "SAT-Sampler aided language for experimental design, targeted for Psychology & Neuroscience ". In particular, we were
-talking about software engineering, and the work that Annie was doing to test
-SweetPea and increase her confidence that the implementation is correct! The
-topic of how exactly one goes about proving a compiler correct came up, and I
-realized that I couldn't think of a high-level (but _concrete_) overview of what
-that might look like. Also, like many compilers, hers is implemented in Haskell,
-so it seemed like a good opportunity to try out the really cool work presented
-at the colocated conference CPP'18 (Certified Programs and Proofs) titled
-["Total Haskell is Reasonable Coq" by Spector-Zabusky, Breitner, Rizkallah, and
+a "SAT-Sampler aided language for experimental design, targeted for Psychology &
+Neuroscience ". In particular, we were talking about software engineering, and
+the work that Annie was doing to test SweetPea and increase her confidence that
+the implementation is correct! The topic of how exactly one goes about proving a
+compiler correct came up, and I realized that I couldn't think of a high-level
+(but _concrete_) overview of what that might look like. Also, like many
+compilers, hers is implemented in Haskell, so it seemed like a good opportunity
+to try out the really cool work presented at the colocated conference CPP'18
+(Certified Programs and Proofs) titled ["Total Haskell is Reasonable Coq" by
+Spector-Zabusky, Breitner, Rizkallah, and
 Weirich](https://arxiv.org/abs/1711.09286). They have a tool (`hs-to-coq`) that
 extracts Coq definitions from (certain) terminating Haskell programs (of which
-at least small compilers hopefully qualify).
+at least small compilers hopefully qualify). There are certainly limitations to
+this approach (see Addendum at the bottom of the page for some discussion), but
+it seems very promising from an engineering perspective.
 
 The intention of this post is twofold:
 
@@ -37,7 +40,9 @@ The intention of this post is twofold:
    this simplified scenario could cover many cases of DSLs, and understanding
    the subtleties that come up should be much easier once you understand the
    basic case!
-
+
+**The intended audience is: people who know what compilers are (and may have
+implemented them!) but aren't sure what it means to prove one correct!**
 
 > All the code for this post, along with instructions to get it running, is in
 > the repository