> Types are checked before program execution. I think this definition is very, very standard, and in keeping with the type theory view.
This is a common informal understanding of the distinction, but when types are checked is not a property of a language and does not agree with the type theoretic definition of what a type system is. For example, you can defer type checking of Haskell programs until runtime [1]. Does Haskell suddenly become a dynamic language just because you decided to check types later even though your code is the same and the program behaves the same? No. What makes Haskell static is the fact that it comes with a set of rules that assign a proof of type-correctness to every valid Haskell program. When or even if you choose to check whether those rules are followed is not the deciding factor.
Similarly, the same Python 3 program can be run with or without running mypy on it first. The Python language is the same either way and a correct program will behave exactly the same since running mypy has no effect on program execution. Does whether Python is a dynamic language or not depend on whether I happen to have run mypy on it first? In this view, the adjectives "dynamic" and "static" do not describe the language and its semantics, they describe how one happens to use it.
> > Being able to describe and annotate types doesn't make a static type system. A static type system is a way of associating with each valid program a proof that there will be no runtime type errors (or at least that certain entire classes of runtime errors will not occur).
> These two statements seem to contradict each other. Adding the type annotations is exactly what allows mypy to associate a proof with code.
Type annotations are neither necessary nor sufficient to be able to type check a program. Type annotations are almost entirely unnecessary in Hindley-Milner languages (ML, Haskell), yet these are very much static languages—these are the languages of type theorists. Conversely, the mypy developers describe mypy as a "type linter" [1] for a reason: mypy is not what type theorists would consider to be a "type checker" precisely because you cannot associate a proof of the lack of type errors with every valid Python program. You can give a proof of the correctness of some programs, but that’s true in any language, so if that’s the criterion for being “static” then every language is static, so the term is meaningless.
> I don't think the definition is useless... it seems entirely consistent with gradual typing.
This HN post about gradual typing is relevant and worth reading: https://news.ycombinator.com/item?id=8595116. Mypy has optional typing, not gradual typing because the Python type system is not complete, even with type annotations. Perhaps you disagree with this perspective and consider Python 3's types to be "real types" and believe that mypy is a "real type checker". In that case, you are in direct disagreement with type theorists because they consider Python to be a unityped language and would take umbrage at calling mypy a "type checker" insisting instead that it is merely a "type linter". This is exactly why I feel that the type theoretic perspective should be broadened to consider systems like mypy to be "real" type systems, albeit dynamic ones, and that they should be studied and formalized rather than dismissed with unhelpful terms like "unityped".
[1] https://ghc.haskell.org/trac/ghc/wiki/DeferErrorsToRuntime
[2] http://mypy.readthedocs.io/en/latest/basics.html