summaryrefslogtreecommitdiffstats
path: root/content/zettel/3a5e.md
diff options
context:
space:
mode:
Diffstat (limited to 'content/zettel/3a5e.md')
-rw-r--r--content/zettel/3a5e.md15
1 files changed, 15 insertions, 0 deletions
diff --git a/content/zettel/3a5e.md b/content/zettel/3a5e.md
new file mode 100644
index 0000000..5c6bab6
--- /dev/null
+++ b/content/zettel/3a5e.md
@@ -0,0 +1,15 @@
++++
+title = "Preservation of safety"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a5d"]
+forwardlinks = ["3a5f"]
+zettelid = "3a5e"
++++
+
+This is the preservation of types and memory safety throughout the
+compilation. This is weaker than proving that a specification holds, and
+therefore also weaker than proving the backward simulation between the
+languages. Therefore, this is also implied by having the backward
+simulation.