Hello Python enthusiasts! As a theoretical computer scientist with some experience on software verification, I’m fascinated by the intricacies of static typing in Python. While I’ve previously worked mainly outside the traditional type-checking realm (in things like bounded model checking), I’ve recently been thinking about something that I believe could contribute to the ongoing effort in typing formalization and standardization. It’s ambitious, but isn’t that where the fun begins? I’d love to hear your insights on its feasibility, what I have overlooked, and any directions or resources you might suggest.
Idea: Provide a level of operational semantics for Python that tracks the types of values, but is able to “execute” Python constructs at the type level. That is, it would not execute using concrete values but types.
Now, if this sounds very similar to what type inference in the existing type checkers does, that’s because it is. The crucial difference would be allowing to execute the type inference using either type annotation level types or Python runtime level types.
This would allow for expressing formally claims such as “no correctly annotation-typed program [without known-unsafe constructs X, Y or Z] can cause a runtime type error”; or that “any value statically typed as X will have a runtime value belonging to set S”. I hope that much of these could be verified using automated theorem proving instead of manual labor in a proof assistant.
(NOTE: For now, assume every sentence contains a disclaimer “in the absence of Any”.)
Goal:
- Sanity check of the typing specification. By expressing the properties in formal language, we certainly need to be able to fully understand what the annotations supposedly mean. This should help discover any gaps in specifications.
- Keeping us informed of exactly what constructs in the annotation system allow for unsound behavior (runtime type errors despite type checking correctly).
- Allow people working on the type system or the Python language to understand what kinds of effects their proposed additions or modifications to the language would have on type safety, i.e. if it opens new avenues of unsoundness.
- Perhaps a formal, machine readable formal specification of the type system would allow synthesizing type checkers from it. That may or may not be useful.
Personally, I’m mostly tickled by point (3).
Random thoughts on the “How”:
I’ve been looking into parsing Python. Clearly a lot of this work must be already done by existing type checkers, so I initially looked into getting dumps from them. That may still be the best approach.
I tried ast and RustPython’s parser. They seem to give approximately the same information. One aspect that is clearly somewhat difficult, at least given the tools that I know of, is mapping variable names to common variables, in that ast only tells us that we’re referring to an identifier “foo”. I think some of that may be difficult given the dynamic nature of Python, but clearly the static analyzers tackle it somehow.
One idea I got today: If I’m not mistaken, I think it should be possible to track the type annotations down to the bytecode level, having a stack of type annotations. Reasoning on the stack machine should be a lot easier than reasoning on the AST level. The details are a bit hazy to me still, particularly because I only understand Python bytecode at a very general level, but I think this might sidestep some complexities like variable scopes and MRO in the simulation phase. On the negative side, it leaves a gap between the AST and the bytecode that needs to be filled (but then, dividing the problem in two halves isn’t necessarily bad).
Questions:
- Does this sound theoretically feasible? Am I missing some reason why it’s not?
- Would you consider such a tool useful? What do you think of the 4 goals I listed?
- Do you have any ideas on the tracking variables topic?
- Has anyone thought about tracking type annotations on the bytecode level? Is there some reason why that necessarily loses information?
