main’s Parameters Are the Command Line; Its Preconditions, Carried Back as Any Function’s Are, Are Checked Where the Words Arrive, a Breach Ending the Program With Status 2Status: Accepted
Date: October 17, 2026
Answers: whether main may take parameters, how the words a program is
started with reach them, and what an assert about them is (issue
#635)
Related:
Part I 5.1 (subject and options; an option’s default);
ADR-269 D5, D6, D14-D21 (a claim about parameters is the
caller’s; data from outside is checked where it arrives; a claim is carried
back to the entry); ADR-318 (a default is a build-time value);
ADR-010 (cli::args is trusted); ADR-285 D36
(int); Part III 14.2, 17.1 (std::cli, the shape of a number in text),
A.2 (how the program ends)
fn main(a: int) { assert(a > 0) … } reads as the program takes a number,
and it must be above 0. For any other function that is what it means: the
assert is a precondition, written in the ledger, proved by every caller and a
fact in the body after it. main’s caller is the person at the command line,
who is not in the program. Today main takes nothing, every program reads
cli::args() and converts, checks and explains by hand, and a main with
parameters is not specified at all.
| Tool | Form | A wrong word | Help |
|---|---|---|---|
| Rust with clap (derive) | a struct with attributes, Args::parse() |
a message and exit status 2 | from doc comments |
| Swift ArgumentParser | a struct with @Argument, @Option, @Flag; validate() |
a message and status 64 | from help: texts |
| Python typer | the function’s parameters: positional without a default, --name with one |
a message and status 2 | from the docstring |
Go flag |
variables registered, flag.Parse() |
written by hand | from a description |
| C; Nikaia before this record | a list of strings | written by hand | written by hand |
None of them makes the check a fact for a prover.
| Option | Example | Why it lost | See |
|---|---|---|---|
main takes nothing; parameters refused |
let a = parse(cli::args().nth(1) ?? "") |
every program writes the same conversion, check and message, and a claim about the number documents nothing | D1 |
main(args: Vec[String]) |
C, Java | a list of untyped words; a claim about it describes no interface | D1 |
A breach of main’s precondition panics |
assert(a > 0) aborts with status 101 |
a wrong word from a person is not a defect of the program (ADR-269 D6) | D4 |
Only an assert at the top of main counts |
positive(10 + a)’s claim stays a panic |
main would be the one function whose contract is not carried back |
D3 |
A subject T? is a required word |
fn main(name: String?) and prog refused |
the ? would say nothing a reader could rely on; a positional word left out is what null means |
D1 |
Exit status 64 (EX_USAGE) |
Swift, BSD | 2 is what clap, typer, getopt tools and shells’ builtins give, and what scripts already test |
D4 |
| Short flags, subcommands, enums from the start | -v, prog build, --mode fast |
every rule of a parser is language and stays; the first step takes what Part I 5.1 already has | §6 |
main’s parameters are the command line.main’s subject parameters (Part I 5.1) are the program’s positional
arguments, in order, each required unless its type is T?: such a
subject may be left out at the end and is then null. Its options are named arguments,
--name value or --name=value, each taking its default when left out; an
_ in a name is written - there (max_depth is --max-depth). An option of
type bool is a bare --name, which sets it to true; --name=false sets it
to false. Named arguments may stand anywhere among the positional ones, and
-- ends them: every word after it is positional. A word that is - followed by a digit is a value, never a name, so prog -3 passes -3. A word that names no option
is a wrong word (D4).
A parameter of main is int, a fixed-width integer, f64, bool,
String, or one of these behind ?; the last subject parameter may be
Vec[T] of one of them, which takes every positional word left, none
included. A number is read in the shape std reads one from text (Part III
17.1) and must fit its type. A subject of type T? stands after every
required subject and before a last Vec[T]. Any other type, a ref
parameter, a required subject after a T? one, and a parameter of main on a
target that has no command line (wasm32-unknown) are refused while the
program is built (NK1273); so is an option named help (NK1274).
main’s preconditions are derived as every function’s are.What becomes a precondition of main is what ADR-269 D5 and D14-D21 make one
for any function: a claim carried back to the entry - through lets,
branches, guards and the preconditions of the calls it makes - that then reads
only parameters, at least one of them, with its path; one that reads none the
prover decides, proved or refuted as any claim is. assert(a > 0) at the top is one;
positive(10 + a)’s assert(whole > 0), carried back through example, is
10 + a > 0. In the body each is a fact, as it is in any function.
Before main’s body runs, the words are read into the parameters and every
precondition of main is checked; this is the check where outside data
arrives that ADR-269 D6 asks for, so a claim about main’s parameters is not
refused with NK1202. A word missing, a word left over, a word that is not of
its type, or a precondition that does not hold, prints one line to standard
error in the program’s terms - the parameter, the claim as written, the value
given, and for a claim carried back the assert it came from - then the short
usage, and ends the program with exit status 2. Nothing of the body has
run: no cleanup is owed and none runs.
--help and -h print the program’s name, the /// lines above main, and
each parameter with its type, its default and its preconditions, then end the
program with status 0. --help after -- is a positional word.
main’s parameters, defaults and preconditions are written in
nikaia.contracts as any function’s are, so a change to what a program
accepts is a ledger diff in review.
main inside the program is an ordinary call.A test or another function that calls main(5) proves its preconditions as
it proves any callee’s. cli::args() still returns every word the program was
started with, so a program may read them itself, with or without parameters on
main.
main is a function; its contract is derived,
written and used as every function’s is (D3, D6). Only its caller differs,
and that caller is outside the program, so the check stands where the words
arrive (ADR-269 D6) and fails as a message, not as a defect (D4).cli::args().main’s
preconditions are checked, 17.1 that std::cli reads main’s
parameters, A.2 exit status 2; Part III’s table carries NK1273 and
NK1274.main’s body,
in the lowering of main and in std::cli; a help text; the report of
--asserts. A program whose main takes nothing pays nothing.-3 is a value).Not decided here: short flags (-v), subcommands, a data-less enum as a
choice of words, environment variables as defaults, a version flag, and
whether --help lists a default that is not a literal.
Decided October 17, 2026 (#635).