Beginning with a set of interactive rewrite rules, Greg Meredith discusses his work with Mike Stay to derive a proof theory that exhibits a Curry-Howard style correspondence. Specifically, it enjoys a cut-elimination property that mirrors the notion of compute in the rewrite rules. Isaac DeFrain and Christian Williams join the conversation. Visit the blog for the corresponding slides.