MATT: Hmmm, but what parts should I talk about? HOLLY (WALKING INTO THE ROOM): "I've got a few questions." MATT: "Oh, this is my wife, Holly, who's a social worker. So I'm sure she'll have great questions. I'd better answer them; after all, she's the boss." HOLLY: "Ugh, I hate trying to make sense of guard proof failures! I tried something once but it didn't seem to work right." MATT: [6.2 The guard-debug utility....] HOLLY: "That's nice, but I want to avoid some of those proof obligations completely!" MATT: [6.2 Ec-call, a wrapper....] HOLLY: "While we're on the subject of guard proofs, I hate it how sometimes I can't tell the reason my defun is failing. Is it because of the termination proof or the guard proof?" MATT: [6.3 Failure messages printed for defun....] [BREAK FOR DEMO] MATT: "There; does that clear everything up?" HOLLY: "That's nice. Now I want to do higher-order programming in ACL2!" MATT: [6.4 ACL2 has a :logic mode utility, oracle-apply....] HOLLY: "Sometimes I go to The Container Store and buy boxes that hold other boxes. Why doesn't that work for stobjs?" MATT: [6.2 The defstobj event ... permits stobjs....] HOLLY: "Math is hard! Rewriting should be easy. I'd sure like to do congruence-based rewriting even for functions that return multiple values." MATT: [6.4 Congruence rules ....] HOLLY: "Sometimes USE hints produce long, noisy proofs." MATT: "Have you tried BY hints?" HOLLY: "They suck!" MATT: "Correction: They USED TO suck!" MATT: [6.3 :By hints are intended....] HOLLY: "Case splits are killing me. What can I do?" MATT: [6.3 ACL2’s proof output indicates splitters] HOLLY: "I love getting new versions of ACL2. It's so much fun reworking my proofs FOR HOURS ON END. Yes, I'm being sarcastic!" MATT: "Wow, Holly is never sarcastic. And by the way, I'm not being sarcastic. We'd better make development copies of ACL2 available between releases, for harmony at home." HOLLY: "Oh, you're the best husband EVER!" MATT: "Uh oh, now I guess she's being sarcastic." MATT: [6.3 ACL2 is now available between releases....] HOLLY: "I guess you've answered my questions for today. Except, I have one more: Is Emacs good? (Sorry, he made me ask that.)" MATT: "No, I prefer Eclipse. Now I'm really being sarcastic! Come to my Rump Session talk for an example of how great Emacs is." HOLLY: "If Emacs is so good, how come it hasn't solved poverty yet?" MATT: "I'm sure it will. Emacs solves everything." MATT: Quoting the paper: We also appreciate contributions by the user community to the large body of Community Books [2]. These books put demands on the system and help us to test improvements. MATT: "I also appreciate contributions by Holly. Take a bow, Holly!" MATT: "Thank you all for your attention. I hope you find the paper to be helpful."