What Bend should do

Provide a pure way to interpret an IO program against an explicit modeled world, so laws can describe its observable behavior: exit status, stdout, stderr, and decisions based on arguments, environment variables, or terminal properties.

For example, a small command-line program could prove that an unknown option writes an uncolored diagnostic to stderr and exits with status 2:

# Proposed API sketch, not code supported by Bend today.
# Main.main is the same entry point used by the executable.
law usage_error:
  {IO.model(
    World{
      args: ["pkg", "--frob"],
      env: [],
      stdout_tty: False{},
      stderr_tty: False{}
    },
    Main.main())
   == Ran{
     code: 2,
     out: "",
     err: "error: unexpected argument '--frob' found\n"
   } : Ran}

World, Ran, and IO.model are illustrative names; the request is for the capability, not this exact API.

Why

Laws over a program's pure core can prove parsing, validation, and formatting while leaving mistakes in the IO shell uncovered: sending a diagnostic to the wrong stream, returning the wrong exit status, continuing after an exit, or emitting color into a pipe. Those behaviors currently need execution tests, often with separate TTY fixtures.

Bend already supports laws equating IO terms: the hello-world demo equates main() with IO.print("Hello, world!"). The missing piece is a pure semantics that supplies effect results and reduces the resulting observations to data, allowing a law to reason about a whole interaction.

There is also an import boundary: user-defined host effects anywhere in a proof's import graph make the verdict fail, even when unused. #1558 explicitly preserves that rule. An IO shell using such effects therefore cannot simply be imported into its laws. Terminal queries are one concrete example, discussed in #1464.

A useful first scope

• Supply IO.args and IO.get_env results from the modeled world, with defined behavior for missing variables.
• Interpret IO.print, IO.write, and IO.print_err, preserving exact output and newline behavior on each stream.
• Model normal completion, IO.exit, and IO.die, including their exit codes, diagnostics, and the fact that termination skips the remaining continuation.
• Supply terminal properties independently for stdout and stderr, so a redirected stream and a terminal can coexist in one fixture. Since these queries currently require custom effects, define a supported way to give an effect a pure model without bringing its host implementation into the proof graph.

The model should interpret the same program used in production. Maintaining a separate pure copy of the IO shell would leave the connection between the two unproved. Unsupported effects should be rejected or explicitly represented as unsupported, never silently treated as successful.

A small demo could prove the example above, then show that swapping stdout and stderr, changing the exit code, or adding an ANSI escape to the piped diagnostic breaks its proof. Additional laws could cover successful help output and an environment-controlled color choice.

These would be proofs about the program under the stated effect model. Tests comparing the model with the C and JS implementations would still be needed to establish that those implementations follow the modeled contract.