And yep --- one way to interpret the technique is that we're carrying out structurally inductive proofs on imperative code. It's (comparably) easy to do structural induction on functional code (think Coq, Lean) because functional code is (usually) pure and written in an explicit structurally inductive style: match on the input, do some loop-free work, then tail-recurse on the rest of the structure.
In this setting we're working with imperative code that mixes loops, side effects, in-place heap mutations, etc., so automatically recovering a valid structurally inductive proof from that messy soup of impure imperativeness presents some unique challenges.
(There are some technical arguments for why the theory is formally closer to proof by infinite descent rather than structural induction, but I don't personally think the distinction is very important.)
FWIW this broader idea of bringing structural induction-like reasoning to analysis of imperative code has been slowly gaining steam over the past few years, especially the Chakraborty et al. and Ish-Shalom et al. techniques we cite in the paper. It works very well for this class of monotonic data structure operations, but unfortunately it doesn't really help for operations like sorting or rehashing, where there's a more "global" modification to the heap structure.
love to see it, there's a huge opportunity in marrying this kind of traditional static analysis with AI tooling
like, literally years' worth of research that has mostly been ignored by industry because it's too complex / has too many false positives
both of which are problems that AI can dramatically mitigate
It sounds like they reinvented structural induction? Regardless, stirling work producing a real world tool and testing it on real codebases.
(Author:) thanks for the kind words!
And yep --- one way to interpret the technique is that we're carrying out structurally inductive proofs on imperative code. It's (comparably) easy to do structural induction on functional code (think Coq, Lean) because functional code is (usually) pure and written in an explicit structurally inductive style: match on the input, do some loop-free work, then tail-recurse on the rest of the structure.
In this setting we're working with imperative code that mixes loops, side effects, in-place heap mutations, etc., so automatically recovering a valid structurally inductive proof from that messy soup of impure imperativeness presents some unique challenges.
(There are some technical arguments for why the theory is formally closer to proof by infinite descent rather than structural induction, but I don't personally think the distinction is very important.)
FWIW this broader idea of bringing structural induction-like reasoning to analysis of imperative code has been slowly gaining steam over the past few years, especially the Chakraborty et al. and Ish-Shalom et al. techniques we cite in the paper. It works very well for this class of monotonic data structure operations, but unfortunately it doesn't really help for operations like sorting or rehashing, where there's a more "global" modification to the heap structure.