main’s parameters are the command line; its preconditions are checked where the words arrive, a breach exits with status 2Open and answer this issue on GitHub.
ready · opened 2026-10-17 · updated 2026-10-17 · 1 comment
The owner wrote, as the next target after #632/#633:
fn main(a: int) {
assert(a>0)
let b = 4*example(a)
let c = (0*4+1)
assert(c==1)
assert(b>40)
println(f"Hello, Nikaia! {b} {c}")
}
fn positive(whole: int) -> int { assert(whole > 0); return whole }
fn example(a: int) -> int { let whole = 10 + a; return positive(whole) }Checked with the compiler on October 17, 2026 (with i64 for int):
nikaia check accepts fn main(a: i64); nikaia run fails in rustc: main function has wrong type, expected fn(). No ADR and no part of the specification says whether main takes parameters; emit_entry.nika treats only a main without arguments, options and return type as the entry.--asserts: assert(a > 0) checked at run time: main has no callers; assert(c == 1) proved (#632 step 1); positive’s claim is carried back to example as 10 + a > 0 and proved at the call; assert(b > 40) checked at run time. With 4 * (10 + a) written out, b > 40 is proved: the fact a > 0 already flows. What remains for b > 40 is ADR-359 D1-D3 (#632); int is #630.The owner’s direction: an assert about main’s parameter is documentation, the contract with the caller (checked at run time, where the arguments arrive), and a fact for every later proof; the contract is derived by the ordinary rules of carrying back, as for any function or method. A decision basis compared clap (derive), Swift ArgumentParser, Python typer and Go flag; the owner chose: parameters of main are the command line (option C), exit status 2 for a wrong word, a small first scope.
ADR-360, specification Part I 5.5, Part III 14.2, 17.1, A.2, NK1273, NK1274:
--name value / --name=value with their defaults, _ written -, a bool option a bare --name; -- ends named words; - followed by a digit is a value.int, fixed widths, f64, bool, String, these behind ?, a last subject Vec[T]; numbers in std’s text shape; anything else refused (NK1273), as are an option help and two options with one name (NK1274), and parameters on wasm32-unknown.main’s preconditions are derived as every function’s (ADR-269 D5, D14-D21): carried back to the entry, reading only parameters.NK1202; a breach or wrong word: one line on stderr (parameter, claim, value, the assert it came from), short usage, exit status 2, no body ran.--help/-h from /// above main, types, defaults, preconditions; status 0.main in the program is ordinary; cli::args() unchanged.Not decided: short flags, subcommands, enums as choices, environment defaults, a version flag.
main per D2; NK1273, NK1274 (codes reserved, text in Part III’s table). Tests: each refused type; help; max_depth + max-depth; wasm32-unknown.main’s carried-back preconditions are reported by --asserts as precondition of main, checked where the words arrive (not checked at run time: main has no callers), and are facts in the body. Test: the owner’s program above (once #630 and ADR-359 D1-D3 are in) reports a > 0 as main’s precondition, b > 40 proved; a variant without assert(a > 0) reports 10 + a > 0 as main’s precondition.std::cli: Rust fn main() reads std::env::args, fills the parameters per D1/D2, checks the preconditions, on failure prints the line and usage to stderr and exits 2; --help/-h print the help and exit 0; then calls the program’s main body. Tests (run the binary): prog 5 runs; prog / prog x / prog 5 6 / prog -3 exit 2 with the message; prog --times=3 5, prog --verbose 5, prog -- 5; prog --help output and status 0; a precondition carried back from a callee names the assert it came from.main’s parameters, defaults and preconditions in nikaia.contracts.lower-std, commit package.rs.examples/ (no version raise): move the cli::args().nth(1) ?? "…" programs to a main option where it reads better.Order: after #630 (int); step 2’s full test after #632’s D1-D3.
Built in 42aa0fa (step 2, prover) and 0f78405 (steps 1, 3, 4, 5), with i64 and the other types:
check_main.nika. NK1273 covers a struct, HashMap, tuple, ref, a Vec that is not the last subject, and Vec[Vec[..]]. NK1274 covers an option named help. Tests are in crates/nikaia/tests/main_parameters.rs.prover_walk.nika no longer sets “main has no callers”, so main’s preconditions are carried back by the ordinary machinery. --asserts says precondition of main, checked where the words arrive, and assert(b > 40) after assert(a > 0) with 4 * (10 + a) is proved.emit_entry.nika and std::cli (Interface, Param, Words). Run-the-binary tests cover prog 5, missing, x, 5 6, -3, --times=3, --be-loud, --, --help/-h, an optional subject, a Vec rest, f64, String?, and a carried-back precondition naming assert(whole > 0) in positive.main’s signature, defaults, requires and from.package.rs is committed.Still missing:
int (#630): int is already on the checker’s list of word types (main_word_type), but there is no test with int. If int lowers to something other than i64, std::cli::Word needs an impl for it. The owner’s program as written (step 2’s full test) waits on #630 and ADR-359 D1-D3.assert(a > 0): 10 + a > 0 is main’s precondition in the ledger, in --help, and in the exit-2 message. But --asserts lists asserts by line and has no row for a carried-back precondition. positive’s assert still reads precondition of positive: proved at every call. A row for a computed precondition of main would be new prover-report work.NK1273 on wasm32-unknown: no check exists. Every build for that target is refused before the source is read (Target::unbuildable).NK1274 for “two options one name once _ is -“: a name cannot contain -, so max_depth + max-depth does not parse. The check is in place but cannot be reached.Generated by Claude Code