Verification and evidence

A program that compiles has not been shown to be correct. Climb the ladder as far as the risk requires, then say where you stopped.

The ladder

Level 4 is where most of the value is. Levels 1 to 3 are cheap and prove very little.

Self-checking programs

The shipped examples are tests. They compute, check, and return a distinct code per failure:

function main() -> i32 {
    let result: f64 = simulate()

    if result != result {
        println("FAIL: state became NaN")
        return 1
    }
    if fabs(result - 2.0) > 1e-6 {
        println("FAIL: expected 2.0")
        return 2
    }

    println("    OK: converged to the closed-form value")
    return 0
}

Distinct codes mean the CI failure tells you which check broke without reading the log.

Running the suites

flow test --strict --verbose    # transpile plus clang, fail on type errors
flow test --tier1               # transpile only, fastest
flow test-runtime               # compile and execute
flow test-lang                  # tests/lang/, strict transpile plus run
flow test-python                # Python unit tests
flow test-mlir                  # needs LLVM
flow test-gpu
flow test-interop
flow test-all                   # everything

Add --sanitize=ub,asan,tsan to compile-and-run tests when memory or concurrency is involved.

Run the suite once, read the output, and act. Do not loop a suite waiting for a different answer.

Checking numerical claims

Pick at least one:

• a closed-form answer for a simplified case;
• a conserved quantity that should stay flat;
• convergence under a halved step size;
• a known qualitative behaviour, such as a decaying envelope or a limit cycle;
• agreement with a second method.

examples/evolution/bouncing_ball.flow compares interpolated impact times against the closed-form sequence and fails if they drift. That is the standard to match.

Safety profiles

flow show-flags --profile=safety
FLOW_PROFILE=safety flow compile program.flow
flow analyze build/program.c --standard=misra-c-2024 --fail-on-violation

Apply these in proportion to risk. A demo does not need MISRA. Anything headed for a device does.

Auditing a claim

When asked whether Flow does X, classify it honestly:

Give the file and command that support the verdict. If two documents disagree, trust the one the test agrees with and say the other is stale.

The report

Every completed piece of work ends with:

• the exact command, environment variables included;
• the real output, trimmed but not paraphrased;
• what was checked and what was not;
• any limit worth knowing.

Never describe planned behaviour as shipped. Never call a compile a pass.