> What about to-be-defined "globals"? (Will you have to "pre-declare" them?)
Globals are not defined and not declared in Lua. They always exist, with nil values unless assigned something else. Which is precisely why they are a problem.
Because they are not declared, they cannot be pre-declared. You could probably say that this proposal makes it possible to have globals declared (without "pre") before they are used (even though it is not solely about globals). Which is good, because it solves the problem.
> Because _ENV can change dynamically, you cannot determine at compile time what names will be valid
Regardless of the proposal, the compiler knows statically what names are global names; those names will be statically converted to _ENV.names. The run-time value of _ENV of irrelevant, the proposal is about statically permitted names.
> What exactly is gained over the current possibilities of _ENV?
A. Static (compile-time) guarantees.
B. Usability. I am not sure you will easily agree, but the _ENV gyrations in your post are magic incantations to a typical Lua user.