1 files changed, 33 insertions, 0 deletions
diff --git a/content/zettel/3a1a.md b/content/zettel/3a1a.md
new file mode 100644
index 0000000..f3f6198
--- /dev/null
+++ b/content/zettel/3a1a.md
@@ -0,0 +1,33 @@
++++
+title = "Issue with Main"
+date = "2021-02-17"
+author = "Yann Herklotz"
+tags = []
+categories = []
+backlinks = ["3a1"]
+forwardlinks = []
+zettelid = "3a1a"
++++
+
+the `main` function in CompCert can not arguments any arguments. In the
+rules for programs going wrong initially, if the initial state cannot be
+constructed, then the program will go wrong, which means that none of
+the correctness proofs can be said to hold.
+
+``` coq
+| program_goes_initially_wrong:
+    (forall s, ~initial_state L s) ->
+    program_behaves (Goes_wrong E0).
+```
+
+The initial state can also only be constructed if the signature of the
+first function that is called is of `signature_main`, which can only be
+of the function type without arguments.
+
+``` coq
+Inductive initial_state (p: program): state -> Prop :=
+  | initial_state_intro: forall b f m0,
+      ...
+      funsig f = signature_main ->
+      initial_state p (Callstate nil f nil m0).
+```