3. I didn’t like the intro—you mostly end up pitching other peoples’ work.
5. Put high/mid-level on the slide. That’s the key thing! Otherwise you don’t separate from others.
6. Rewrite db came out of nowhere.
6. Need visual for most bug dense as well.
7. You make it sound like CompCert is you.
8. You haven’t introduced proofs yet, makes your work seem trivial. What do you mean by local/global correctness?
16. Point out that you only want the %eax values, you don’t care about %ecx
19. What does it mean for a register to be dead?
20. Are parametric rewrites new? Why add it to the slides?
26. Could have used the description of what a proof is waaaaaay earlier
28. Is the measure and finiteness things due to just termination? Is there any value in lifting that? I think the C standard is pretty flexible here.
31. Better separate theorems, checks, and assumptions (calling convention, liveness termination, etc)
40. The original Peek talk had a pretty complex structure, in a defense I am totally lost keeping this story in mind while still trying to connect it to the higher-level whole-thesis story.
48. Tough to read the CompCert code fast enough
49. I’m confused why the new semantics are an important part of the whole talk.
52. Unreadable much text
53. Concerned about the handling of use after free
55. Discussion of what CompCert does when malloc fails
67. Very very cool result. Should be somehow hinted at.
69. The shim point is very good. Should make more explicit that Cminor has a proof theory, so you can also verify your shim.
74. Please do not show code… I am not going to read it and I am going to get lost.
74. Point out that shim is verified.
78. Whole point is reasoning but it’s never on any slide. Would also clarify #79.
79. The definitional / propositional equality thing
79. Could be worth presenting this as a development methodology much earlier.
85. Good description
86. You seem to regularly have a slide just a few more slides later than the questions appear. Prepared, but maybe wrong order.
90. Compare with “Eval compute”
91. Put the actual stuff in the spec, not the LOC
92. Is oeuf_string_to_string and friends verified?