[mirashii]

The thing is that almost always isn't good enough. If it can't prove it, then a human has to be put back in the loop to verify and assert, and on sensitive timelines when you have regulatory requirements on time to acknowledge and resolve CVEs in dependencies.

[woodruffw]

Sure, but I think the useful question is whether it’s good enough for the median Python codebase. I see the story as similar to that of static typing in Python; Python’s actual types are dynamic and impossible to represent statically with perfect fidelity, but empirically static typing for Python has been very successful. This is because the actual exercised space is much smaller than the set of all valid Python programs.