1 files changed, 52 insertions, 0 deletions
diff --git a/notes.org b/notes.org
new file mode 100644
index 0000000..39e93f8
--- /dev/null
+++ b/notes.org
@@ -0,0 +1,52 @@
+Yes! It's loads better! I'm glad I made a fuss! :)
+
+Ok, lots of feedback below, but it's mostly low-level details now. Here goes...
+
+TALK 1: You say "formally verified" but the slide says "formal verification of" which is a bit jarring.
+
+TALK 3: Don't start with "So...". Just launch straight in with "The need for...". (I'm getting such deja
+vu from 2012-ish when I was given exactly the same advice when giving a practice talk for a
+fellowship interview. I started with "So..." and was immediately heckled for it!)
+
+TALK 3: I like the SSD/SSD/HDD example. It's nifty. And perfectly understandable too. I think there
+are one or two bits that could still be slightly optimised, for instance, you say "It will always
+perform the same task" and then "which would always do the same task" a few moments later.
+
+TALK 5: The .v -> FPGA diagram is very good -- I would just change your words from "use logic synthesis"
+to "use a logic synthesis tool" to emphasise that it's not a manual process.
+
+6: The text about "difficult to debug" appears too soon. I found myself reading the text and being a
+bit confused because it didn't match what you were saying. Only introduce the text at the moment you
+talk about it. Same happens on slide 16 -- the diagram appears a few seconds too soon and it
+distracts me from what you're saying.
+
+TALK 7: "we're gonna call 3AC [because RTL is already an established abbreviation in hardware design]"
+
+TALK 14: I still think there's an opportunity for a little bit of humour/showmanship when you make the
+point about the RAM interface. For instance, you could say something like "Actually here is a mildly
+terrifying example of quite how fragile the logic synthesis tools are -- if the RAM interface
+doesn't use this _exact_ Verilog syntax, then the tool won't know to use RAM and will synthesise
+thousands of registers instead, and the circuit will be disastrously inefficient."
+
+TODO 17: Similar comment as before: I recommend making sure that each piece of text only appears at
+the instant you talk about it. Currently I'm reading about "Wrong" while you're talking about
+"Converging" and that's not ideal :)
+
+TALK 20: I like the addition of "bad news" -- that's really helpful for telling the audience how to
+interpret this slide. I suggest beginning this slide by saying which benchmarks you use (and why)
+and emphasise that you can compile almost all of them. And then, when you show the graphs, you need
+to give a bit of time for them to be digested. You were talking about interpreting the results, but
+I was still trying to read the labels on the y-axes. You need to say what the top and bottom graphs
+are showing, say what the three colours of bar mean, whether higher bars are good or bad (and say
+things like "we see that the green bars really high, and way higher than the others"), and say that
+the x-axis shows all 27 benchmarks plus the median. I think you need to spend a good 2 minutes on
+this slide alone.
+
+TALK 22: Rather than "0% (0.03%)", I suggest showing "0.03%" first, explaining what's going on, and
+then striking it out and writing "0%", so the end result looks like ^0.03%^ 0%. (As for Bambu, I'd
+be tempted to drop the 13.7% point altogether, as it's an unnecessary detail. (Let's just be kind to
+them!)) And I'd encourage a little bit of showmanship here -- you could put the "Vericert" text in
+first, leaving the number blank, and then say something "and of course, since this is all proven in
+Coq we'd expect a nice 'zero percent' here...[then introduce the 0.03%]...well ok, that's not quite
+how it worked out at first...but what happened was...". And I'd mention that this is exactly what
+happened when the Csmith people fuzzed CompCert for the first time.