summaryrefslogtreecommitdiffstats
path: root/content/zettel/3a5e.md
blob: 5c6bab6c6fafc796644b9828ad0945d79c3ca1a9 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
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.