Summary

Vera has no way to pause execution, no way to get the current time, and no way to write to stderr. All three gaps were discovered while writing a Conway's Game of Life program — you can print each generation but not animate it, measure rendering time, or report errors to a different stream than stdout.

Proposed API

Add three operations to the existing IO effect:

IO.sleep(@Nat)  ->  Unit             -- pause for N milliseconds
IO.time(@Unit)  ->  @Nat             -- current Unix time in milliseconds
IO.stderr(@String)  ->  Unit         -- write to stderr

Each is a single operation on an existing effect — minimal diff per op, but they compose. A realistic animation loop needs all three:

-- Target 30 FPS frame budget
let @Nat = IO.time(());
render(@Grid.0);
let @Nat = IO.time(());        -- elapsed measurement
let @Int = 33 - nat_to_int(@Nat.0 - @Nat.1);
if @Int.0 > 0 then { IO.sleep(int_to_nat(@Int.0)) } else { () }

IO.stderr is orthogonal but ships together because it's the same one-row addition to the effect's operations dict.

Implementation

• environment.py: Add three entries to IO effect's operations dict:
  • OpInfo("sleep", (NAT,), UNIT, "IO")
  • OpInfo("time", (UNIT,), NAT, "IO")
  • OpInfo("stderr", (STRING,), UNIT, "IO")
• codegen/api.py: Three host imports:
  • vera_io_sleep — time.sleep(ms / 1000)
  • vera_io_time — int(time.time() * 1000)
  • vera_io_stderr — sys.stderr.write(...) + flush
• wasm/calls.py: Wire each to its host import
• Browser runtime (vera/browser/runtime.mjs):
  • sleep: implement via Atomics.wait on a shared buffer (synchronous delay in worker context) or document as no-op in browser
  • time: Date.now()
  • stderr: console.error(...)

Rationale

Every general-purpose language has these three primitives. They're essential for:

• sleep: animation loops, rate limiting (API calls, polling), simulating delays in tests
• time: elapsed-time measurement, frame-budget computation, timestamps for logging, cache expiry
• stderr: CLI error messages that don't pollute stdout (important for pipelines where stdout is data)

These are three independent one-row additions to the existing IO effect. Diff is minimal; empirical evidence (Conway's Life work) shows they're wanted together.