1 files changed, 55 insertions, 0 deletions
diff --git a/content/zettel/3a4.md b/content/zettel/3a4.md
new file mode 100644
index 0000000..017cee6
--- /dev/null
+++ b/content/zettel/3a4.md
@@ -0,0 +1,55 @@
++++
+title = "Hacking CompCert"
+date = "2020-12-10"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a3", "3a"]
+forwardlinks = ["3a5", "3a4a"]
+zettelid = "3a4"
++++
+
+CompCert is built in a way which makes it very easy to hack, meaning one
+can insert extra passes and build on the proofs that they developed.
+There have been many examples of this, for example Compositional
+CompCert \[1\] or CompCertM \[2\].
+
+The main reason that CompCert facilitates this is because they have
+designed the proofs for each of their language translations is a similar
+way, meaning one can adopt the same translation style and get a similar
+proof for ones own intermediate language. In addition to that, CompCert
+contains many helper theorems for proofs of simulation, which are the
+main arguments that are used to prove equivalence. Finally, all the
+proofs of the different languages are composed at various levels,
+meaning that if they are changed, one can compose the proof in a custom
+way that still proves the original property that the behaviour stays the
+same throughout the translations.
+
+<div id="refs" class="references csl-bib-body" markdown="1">
+
+<div id="ref-stewart15_compos_compc" class="csl-entry" markdown="1">
+
+<span class="csl-left-margin">\[1\]
+</span><span class="csl-right-inline">G. Stewart, L. Beringer, S.
+Cuellar, and A. W. Appel, “Compositional CompCert,” in *Proceedings of
+the 42nd annual ACM SIGPLAN-SIGACT symposium on principles of
+programming languages*, in POPL ’15. Mumbai, India: Association for
+Computing Machinery, 2015, pp. 275–287. doi:
+[10.1145/2676726.2676985].</span>
+
+</div>
+
+<div id="ref-song19_compc" class="csl-entry" markdown="1">
+
+<span class="csl-left-margin">\[2\]
+</span><span class="csl-right-inline">Y. Song, M. Cho, D. Kim, Y. Kim,
+J. Kang, and C.-K. Hur, “CompCertM: CompCert with C-assembly linking and
+lightweight modular verification,” *Proc. ACM Program. Lang.*, vol. 4,
+no. POPL, Dec. 2019, doi: [10.1145/3371091].</span>
+
+</div>
+
+</div>
+
+  [10.1145/2676726.2676985]: https://doi.org/10.1145/2676726.2676985
+  [10.1145/3371091]: https://doi.org/10.1145/3371091