Point 1 is explained, at a high level, in the introduction: "In Hummingbird, user-provided type annotations actually execute at run-time, adding types to an en

Point 1 is explained, at a high level, in the introduction: "In Hummingbird, user-provided type annotations actually execute at run-time, adding types to an environment that is maintained during execution. As metaprogramming code creates new methods, it, too, executes type annotations to assign types to dynamically created methods. Then whenever a method m is called, Hummingbird statically type checks m’s body in the current dynamic type environment. More precisely, Hummingbird checks that m calls methods at their types as annotated, and that m itself matches its annotated type. Moreover, Hummingbird caches the type check so that it need not recheck m at the next call unless the dynamic type environment has changed in a way that affects m." Personally, I think they're pushing the bounds of what "statically" means, but hey, they do say it's "just-in-time static". It does indeed do the checking before executing the function, it just happens to be immediately before executing the function. A paragraph later: "To ensure our approach to type checking is correct, we formalize Hummingbird using a core, Ruby-like language in which method creation and method type annotation can occur at arbitrary points during execution. We provide a flowsensitive type checking system and a dynamic semantics that invokes the type system at method entry, caching the resulting typing proof. Portions of the cache may be invalidated as new methods are defined or type annotations are changed. We prove soundness for our type system." Based on how their approach works, I don't think Point 2 stands.