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.

Oh ok. So it's not really static at all, they're just calling it that because it sounds better. It's simply dynamic type-checking that checks the types immediately prior to calling the function instead of checking them at the top of the function body. Offhand, it seems that the only benefit to this approach (checking prior to calling the function instead of checking inside the function) is the ability to cache the results and skip checking the same callsite in the future if nothing's changed.

Being able to significantly optimize type-checking for scripting languages like this to the point where you can actually run this in production seems quite valuable. But calling it "static type-checking" is simply wrong. Granted, they're calling it "just-in-time static", but that phrase is contradictory, it would be like saying "dynamic static type checking".

1. When the only way to modify code is to create a new function, this technique would work fine.

2. I think you're right.