> how do they know it's even bounded? Why isn't there a combinatorial explosion?
I don't know - I'm in middle of watching the interview too, but he's moved on from that topic already. I'd guess the 10M vs 1M (or 100M) estimate comes from the curve of total "assertions" vs time leveling off towards some asymptotic limit.
I suppose the reason there's no combinatorial explosion is because they're entering these assertions in most general form possible, so considering new objects doesn't necessarily mean new assertions since it may all be covered by the superclasses the objects are part of (e.g. few assertions that are specific to apples since most will apply to all fruit).