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.