Add content

1 files changed, 27 insertions, 0 deletions

diff --git a/content/zettel/3a7.md b/content/zettel/3a7.md
new file mode 100644
index 0000000..9752273
--- /dev/null
+++ b/content/zettel/3a7.md
@@ -0,0 +1,27 @@
++++
+title = "Translation validation"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3c3", "3a6", "2e1d2", "2e1c6", "1f4a"]
+forwardlinks = ["2e1c1", "3a8", "3a7a"]
+zettelid = "3a7"
++++
+
+Translation validation is a proof technique whereby one can perform an
+unverified translation and verify that the results match after the
+translation using a verified validator. This gives exactly the same
+guarantees as normal verification for a verified compiler, for example,
+because the compiler is allowed to fail. The correctness proofs only
+need to hold if the compiler succeeds.
+
+This means that a proven validator which errors out if it cannot prove
+the equivalence between the input and output of the verified pass also
+allows for a verified pass. One therefore has to show that if the
+verified validator says that the input and output are equivalent, that
+the semantics of the input and output are as well.
+
+Translation validation is often performed by using symbolic execution
+([\#2e1c1]).
+
+  [\#2e1c1]: /zettel/2e1c1