We need a new specification language for summaries. I think just a (pseudo?-)programming language’s API (modules, interfaces, method signatures), but more concise and descriptive than Java, maybe Haskell or OCaml minus quirks (…the academics were this close to an ideal syntax, maybe they should’ve gave up those languages’ LR parsers…)