1 files changed, 24 insertions, 0 deletions
diff --git a/content/zettel/3c3j.md b/content/zettel/3c3j.md
new file mode 100644
index 0000000..1bbe9a9
--- /dev/null
+++ b/content/zettel/3c3j.md
@@ -0,0 +1,24 @@
++++
+title = "Design Trade-offs for the Scheduling Proof"
+date = "2022-11-16"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3c3i"]
+forwardlinks = ["3c3k"]
+zettelid = "3c3j"
++++
+
+There are a few trade-offs that were made during the scheduling proof,
+such as:
+
+-   deciding to use flat predicates instead of a tree-like structure
+-   if-conversion, which is a more self-contained way to prove the
+    translation without having to worry about the performance of the
+    code
+-   The representation of the predicates is also an interesting
+    trade-off, because there are various ways to do this.
+-   Using if-statements or constraints to prove the backwards simulation
+    in the abstract interpretation.
+
+**\*\***