Automatic Asymptotic Analysis
I recently tried to have a research conversation over Twitter -- always a questionable choice -- with an algorithms researcher, spurred by my comment that I was surprised to be able to find no work (at a cursory glance) on automatic deduction or checking of asymptotic runtime analysis. After all, went my thought process, when a TA looks at the solutions to my Graduate Algorithms homework and determines that the pseudocode meets the runtime signature specified in the assignment, a certain amount of it is entirely mechanical. In Constructive Logic at CMU, we use Tutch to give students automatic feedback on natural deduction proofs -- something that's very simple to check by hand but which can be learned much more quickly with a rapid sequence of alternating attempts and feedback. The comment was met with skepticism, which I eventually decided to consider warranted at least to the extent that we want to a) perform analyses that require constructing adversarial input and b) in