Propose rules about main for null-safety (#1146)

Cf. #1120, the rules about `main` impose very few requirements on the signature and the behavior, and the ones that are specified are actually more strict than the implementations.

This PR changes the rules such that obviously type-incorrect declarations of `main` are a compile-time error, and additional signatures (with optional arguments) allowed by the tools are now also allowed according to the specification. It is still a requirement that `main` is a method, and no library can declare a `main` which cannot be the initial function. Also, invocations of `main` are now explicitly required to be type safe (which seems to be implemented already).

Finally, it allows each tool to reject any `main` declaration according to additional implementation specific constraints, which means that no work is required in any tool in order to support this spec change.

Author: eernstg

accepted/future-releases/nnbd/feature-specification.md

@@ -6,6 +6,9 @@ Status: Draft
 
 ## CHANGELOG
 
+2020.08.12
+  - Specify constraints on the `main` function.
+
 2020.08.06
   - Specify error for uninitialized final instance variable in class
     with no generative constructors.
@@ -998,6 +1001,56 @@ These are extended as
 per
 [separate proposal](https://github.com/dart-lang/language/blob/master/resources/type-system/flow-analysis.md).
 
+### The main function
+
+The section 'Scripts' in the language specification is replaced by the
+following:
+
+Let _L_ be a library that exports a declaration _D_ named `main`.  It is a
+compile-time error unless _D_ is a function declaration.  It is a
+compile-time error if _D_ declares more than two required positional
+parameters, or if there are any required named parameters.  It is a
+compile-time error if _D_ declares at least one positional parameter, and
+the first positional parameter has a type which is not a supertype of
+`List<String>`.
+
+Implementations are free to impose any additional restrictions on the
+signature of `main`.
+
+A _script_ is a library that exports a declaration named `main`.
+A script _L_ is executed as follows:
+
+First, _L_ is compiled as a library as specified above.
+Then, the top-level function defined by `main`
+in the exported namespace of _L_ is invoked as follows:
+
+If `main` can be called with with two positional arguments,
+it is invoked with the following two actual arguments:
+
+- An object whose run-time type implements `List<String>`.
+- An object specified when the current isolate _i_ was created,
+  for example through the invocation of `Isolate.spawnUri` that spawned _i_,
+  or the null object if no such object was supplied.
+  A dynamic error occurs if the run-time type of this object is not a
+  subtype of the declared type of the corresponding parameter of `main`.
+
+If `main` cannot be called with two positional arguments, but it can be
+called with one positional argument, it is invoked with an object whose
+run-time type implements `List<String>` as the only argument.
+
+If `main` cannot be called with one or two positional arguments, it is
+invoked with no arguments.
+
+In each of the above three cases, an implementation is free to provide
+additional arguments allowed by the signature of `main` (*the above rules
+ensure that the corresponding parameters are optional*).  But the
+implementation must ensure that a dynamic error occurs if an actual
+argument does not have a run-time type which is a subtype of the declared
+type of the parameter.
+
+A Dart program will typically be executed by executing a script.  The
+procedure whereby this script is chosen is implementation specific.
+
 ## Runtime semantics
 
 ### Weak and strong semantics