1 files changed, 29 insertions, 0 deletions
diff --git a/content/zettel/3a5f.md b/content/zettel/3a5f.md
new file mode 100644
index 0000000..4ffb49d
--- /dev/null
+++ b/content/zettel/3a5f.md
@@ -0,0 +1,29 @@
++++
+title = "Specification for proofs"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a5e"]
+forwardlinks = []
+zettelid = "3a5f"
++++
+
+To build a proof of an algorithm, it can be useful to have a
+specification of the algorithm first, and then prove that this
+specification has the property that one wants to prove. This can be
+useful because the specification is often at a higher level than the
+algorithm itself, and it can therefore be easier to identify it's
+behaviour in the proofs.
+
+However, one more step is needed if this approach is taken, because it
+also has to be proven that the algorithm that one designed does indeed
+implement the specification that was designed. However, this only has to
+be done once, and thereafter the specification can be used to prove any
+other useful properties.
+
+A concrete example for this is the proof from Cminor to RTL in CompCert.
+At the lowest level, there is an implementation of an algorithm that
+does this translation. However, then there is a specification of this
+algorithm using `Inductive` types. The latter is then used to prove that
+the semantics before the translation are equivalent to the semantics
+after the translation.